This page is essentially a copy of Axioms with the Greek letters replaced with Latin letters.
Ax. 1 'Simplification': ⊢ A → (B → A)
Ax. 2 'Frege axiom': ⊢ [A → (B → C)] → [(A → B) → (A → C)]
Ax. 3 'Transposition': ⊢ (¬A → ¬B) → (B → A)
Ax. 4 (inference rule) 'Modus ponens': ⊢(A → B) , ⊢A ⇒ ⊢B
Ax. 5 (inference rule) 'Definitional soundness 1': ⊢(A ≝ B), ⊢C[A] ⇒ ⊢C[B/A], provided that A doesn't occur within the wff B and B doesn't within A
Ax. 6 (inference rule) 'Definitional soundness 2': ⊢(A ≝ B), ⊢C[B] ⇒ ⊢C[A/B], provided that A doesn't occur within the wff B and B doesn't occur within A
Ax. 7 (inference rule) 'Generalization': ⊢A ⇒ ⊢(∀x)A(x), provided that A is either an axiom or a theorem of L1+ZF and is derived from an axiom or a theorem of L1+ZF; 'if A is a theorem, then it is true of anything'
Note: the A cannot be '☐A', otherwise the derived formula wouldn't be well-formed
Ax. 8 'Quantified conditional ': ⊢ (∀x)[A(x) → B(x)] → [(∀x)A(x) → (∀x)B(x)] 'if, for each object x, A being true for that object implies B also being true of that object, then A being true for every object implies B being true for every object'
(More familiar: 'if everything that is A would also be B, then, if everything is A then everything is also B')
Ax. 9 'Distinctness': ⊢[A(b, c, ...) → (∀[x/a])A], provided that 𝛼 doesn't occur in the wff 𝜑
'if a doesn't occur in A, then generalizing on a only doesn't affect the truth of A' (this axiom is trivial)
Ax. 10 'Existence': ⊢ ¬(∀x)¬(x = a) 'it is not the case that everything is not identical to an individual object', in other words, 'something exists'
Ax. 11 'Identity': ⊢ (a = b) → [(a = c) → (b = c)]
Ax. 12 'Left identity for binary relations': ⊢ (a = b) → (A(a, c) → A(b, c))
Ax. 13 'Right Identity for binary relations': ⊢ (a = b) → (A(c, a) → A(c, b))
Ax. 14 'Extensionality': ⊢ (∀x)[(x ∈ A) ↔︎ (x ∈ B)] → (A = B) ' the identity of a set is determined only by its member(s)
Ax. 15 'Replacement': ⊢ (∀x)(∃A)(∀y){ [(∀A)P → (y = A)] → (∃A)(∀y)[(y ∈ A)) ↔︎ (∃x)((x ∈ B) & (∀A)P)] } 'the image of a set under a function is also a set'
Ax. 16 'Union': ⊢ (∀A)(∃B)(∀x){(∃C)[(x ∈ C) & (C ∈ A)] → [x ∈ B)} 'for any set A, there is a set (B) that contains every member x of the members (C) of A'
Ax. 17 'Regularity': ⊢(∃x)(x ∈ A) → (∃y)[(y ∈ A) & ([y ∩ A] = ∅)] 'if a set is nonempty, then it contains a member with which it shares no member in common (that member is the empty set)'
Ax. 18 'Power set': ⊢ (∀A)(∃B)(∀C){(∀x)[(x ∈ C) → (x ∈ A)] → (C ∈ B)} 'for any set A, there is a set (B) that only contains every subset (C) of A'
Ax. 19 'Infinity': ⊢ (∃A){[∅ ∈ A] & (∀B)[(B ∈ A) → (∃C)([C ∈ A] & (∀x){ (x ∈ C) ↔ [(x ∈ B) ∨ (x = B)] } ) ) 'there is a set A that contains the empty set and, for every subset (B) of A, there is another subset (C) of A whose members are all either also contained in B or identical to B',
Remarks: Since the empty set is a subset of A, there is another subset ('1') of A whose member(s) is either just the empty set or all members of the empty set or both, and this subset is contained in yet another subset ('2') of A, whose members are either just '1' or all members of '1', or both, and so on. Thus, A is an infinite set. This axiom is for positing the distinct quantities. Another way of reading this axiom is that there is no largest quantity.
These axioms can be proven from the above axioms using methods outside L1+ZF, and thus they can be proven redundant. However, they are included here so that this system won't need to rely on outside methods.
Ax. 20 'Boundedness' ⊢ (Ⅎx)[¬(∀x)A(x)] 'All occurrences of x in ¬(∀x)A(x) is bounded by a quantifier (in this case, ∀)' (analogous to Ax. 10 of Metamath)
Ax. 21 'Universal quantifier commutation' ⊢ (∀x)(∀y)A[x, y] → (∀x)(∀y)A[x, y] 'the ∀ quantifiers binding to two different variables can be switched'
Ax. 22 'Substitution' ⊢ (x = y) → [(∀y)A(y) → (∀x)[(x = y) → A]] 'if x is identical to y, then, if every y is A then everything identical to y is also A'
Ax. 23 'Quantified distinctness' ⊢ ¬(x = a) → [(a = b) → (∀x)(a = b)] 'if x is distinct from 𝛼, then quantifying over the identity of 𝛼 with 𝛽 doesn't affect its truth' (analogous to Ax. 7)
Ax. 24 'Deduction' ⊢[(𝚪 & A) ⊢ B] ⇒ ⊢[𝚪 ⊢ (A → B)] , where 𝚪 is a (possibly empty) set of wffs, (usually proven as the 'Deduction Theorem', this states that if B was proven from A with the set of premises 𝚪, then the conditional A → B also logically follows from 𝚪)
Based on 1.3 and 1.5
Ax. 25 (inference rule) 'Necessitation': ⊢A ⇒ ⊢☐A , provided that A is a either a non-modal axiom or a non-modal theorem of L1+ZF 'if A is a theorem, then A necessarily obtains'
Note: A cannot be ☐P, otherwise the derived formula would be not well-formed.
Ax. 26 'Kripke axiom': ⊢☐(A → B) → (☐A → ☐B) 'if necessarily, if A obtains then B also obtains, then, if A necessarily obtains then B also necessarily obtains'
Ax. 27 'Necessity': ⊢ ☐A → A 'if A necessarily obtains, then A obtains'
These definitions are for abbreviating certain specific formulas, containing at least one logical operator, using other operators. In a proof, it allows one to substitute a specific string of formula with the specific formula on the other side. Definitions are merely abbreviations provided that both the formula being defined and the defining formula contain at least one logical operator or connective operating on a wff, and that the operator(s) (except for variable-binding operator(s) that bind the same variable on both sides) on each side doesn't also appear on the other side.
The justifications for each definition are given in the Formal Language page.
(A & B) ≝ ¬(A → ¬B)
(A ∨ B) ≝ (¬A → B)
(A ⊻ B) ≝ ¬(A ↔︎ B)
(A ↔︎ B) ≝ [(A → B) & (A → B)]
(∃x)Ax ≝ ¬(∀x)¬Ax
(a ≠ b) ≝ ¬(a = b)
(A ∉ B) ≝ ¬(A ∈ B)
(a ∉ A) ≝ ¬(a ∈ A)
(A ⊆ B) ≝ (∀x)[(x ∈ A) → (x ∈ B)]
(A ⊇ B) ≝ (∀x)[(x ∈ B) → (x ∈ A)]
(A ⊂ B) ≝ [(∀x)[(x ∈ A) → (x ∈ B)] & (A ≠ B)]
(A ⊃ B) ≝ [(∀x)[(x ∈ B) → (x ∈ A)] & (A ≠ B)]
(x ∈ {y | A}) ≝ A[x/y]
∅ ≝ {x | ¬(x = x)}
⊤ ≝ ¬⊥
(A1 ∧ A2 ∧ A3 ∧ ... ∧ An) ≝ [An & (An-1 & (An-2 & (... & (A2 & A1))))]
(A1 ⋎ A2 ⋎ A3 ⋎ ... ⋎ An) ≝ [An ∨ (An-1 ∨ (An-2 ∨ (... ∨ (A2 ∨ A1))))]
(A1 ⩒ A2 ⩒ A3 ⩒ ... ⩒ An) ≝ [An ∨ (An-1 ∨ (An-2 ∨ (... ∨ (A2 ∨ A1))))] & (P = {A1, A2, A3, ... , An}) & (∀x)([(x ∈ P) & (y ∈ P) & (x ≠ y)] → ¬(x & y))
(∀x ∈ y)A ≝ (∀x)[(x ∈ y) → A]
(∃𝜁 ∈ 𝜀)𝜑 ≝ (∃𝜁)[(𝜁 ∈ 𝜀) & 𝜑]
(Ⅎx)A ≝ (∀x)(A → (∀x)A)
⃟A ≝ ¬☐¬A
A[x/y] ≝ {[(x = y) → A] & (∃y)[(x = y) & A]}
(∀*x ∈ P)A ≝ [(∀x)[(x ∈ P) → A] & (∃x)(x ∈ P)]
Wx ≝ [(x ∈ W) & (∀y)[(y ≠ W) → (x ∉ y)]]
☐A ≝ (∀x)[Wx → (∃y)[(y ∈ x) & (y ↔︎ A)]]
◇A ≝ (∃x)[Wx & (∃y)[(y ∈ x) & (y ↔︎ A)]]