This page details the axioms of L1+ZF as a logic. Ax. 1 - 17 are all also axioms used for the system used at Metamath.org for deriving most known theorems of mathematics. These axioms aren't intended to be exhaustive of the foundational primitive concepts.
For a more reader-friendly list, see here.
The following are the truth tables of each of the logical connectives as they are used in classical, propositional logic.
The fundamental connectives here are negation and the material conditional. The conjunction and the disjunction are merely for conjoining two or more SoAs together.
Based on 1.4, the truth value of not-A is the opposite of that of A.
¬⊤ : ⊥
¬⊥ : ⊤
Based on 1.9
In English, this is usually expressed by saying 'if A, then B' or 'A implies B'. These phrases are used to communicate and deduce about
Causation ('if I push the chair, it would move forward' and 'the chair didn't move forward, therefore I didn't push it' )
Causal chains/web ('if Matt was at home (causing him to be in range of the phone's sound), he would have answered the home phone' and 'the phone wasn't answered, therefore Matt wasn't at home')
Supervenience (an object having a macroscopic property A due to its having a microscopic property B, 'if this body of water contains dissolved ions, then it conducts electricity' and 'it doesn't conduct electricity, therefore it doesn't contain any dissolved ions)
Mathematical truths ('if n isn't divisible by 2, then n isn't divisible by 4')
Table
(⊤ → ⊤) : ⊤
(⊤ → ⊥) : ⊥
(⊥ → ⊤) : ⊤
(⊥ → ⊥) : ⊤
Remarks:
Justifications: 'A → B' ('if A, then B') is true (obtains) when the antecedent A and the consequent B are both true, and it is also true whenever the antecedent A is false. 'A IMPLIES B' only indicates that if one knows that A is true, then one can conclude that B is also true regardless of whether or not A is relevant to B in some specific ways. To see why this truth table is correct, check each of its rows:
Row 1: If one knows that A and B both obtain, one can conclude that B obtains after knowing that A obtains, which is exactly what 'A → B' means. Indeed, B's obtaining is not dependent on what the rest of the actual world is like. (you may think that some SoAs' obtaining does depend on the obtainment of other SoAs, but this is confusing the obtainment itself with how the various instantiations of properties contained in the obtained SoA relates to the instantiations of properties contained in another SoA)
Row 2: This row is uncontroversial and intuitive.
Row 3: If one knows that A doesn't obtain and B obtains, one can conclude that B obtains if one knows that A obtains (even though this is impossible to do per already knowing that A doesn't obtain) because:
B's obtainment is not dependent on what the rest of the actual world is like.
a contradiction (A & ¬A) implies any SoAs. (this can be shown even when '&' and '∨' are treated as primitive connectives, i.e. not defined using '¬' and '→')
Row 4: At first glance, this should only be one-way, that is, '(A → B) → (¬B → ¬A)' is true (and used in daily reasoning for eliminating possibilities) but '(¬A & ¬B) → (A → B)' is problematic. However, as above, a contradiction (A & ¬A) implies anything.
Utility of the material conditional: Because of this truth table, the conditional is usable not just for expressing causation and supervenience, but also for expressing logical and mathematical statements.
Row 1, 3 and 4 aren't problematic for daily reasoning because one usually begins with a conditional as a starting premise when reasoning. The commonly used scheme 'if A, then B; not B, therefore not A' starts with a conditional among its premises. A counterfactual conditional sentence in natural languages (a conditional with a false antecedent) formalized using the material conditional would always be true because it deal with the sentence in the actual world, not in another possible world (when a counterfactual is false, it is a conditional that is false in another nearby possible world), and a contradiction implies anything, but this is not a problem because one usually reasons using true counterfactuals (such as in the phone example above).
In conclusion, there are no "paradoxes" of material conditional.
'A and B' is true only when both A obtains and B obtains.
(⊤ & ⊤) : ⊤
(⊤ & ⊥) : ⊥
(⊥ & ⊤) : ⊥
(⊥ & ⊥) : ⊥
'A or B' is true only when either of A and B obtains.
(⊤ ∨ ⊤) : ⊤
(⊤ ∨ ⊥) : ⊤
(⊥ ∨ ⊤) : ⊤
(⊥ ∨ ⊥) : ⊥
'A xor B' is true only when either of A and B obtains but not both.
(⊤ ⊻ ⊤) : ⊥
(⊤ ⊻ ⊥) : ⊤
(⊥ ⊻ ⊤) : ⊤
(⊥ ⊻ ⊥) : ⊥
𝜑 is a tautology (L1=-valid): 𝜑 is true in every interpretation / the truth value of 𝜑 is ⊤ in every row of its truth table / 𝜑 obtains in every possible world
𝜑 is a contradiction (L1=-invalid): 𝜑 is false in every interpretation / the truth value of 𝜑 is ⊥ in every row of its truth table / 𝜑 doesn't obtain in any possible world
𝜑 is L1=-contingent: 𝜑 is true in some interpretation and false in some interpretation / the truth value of 𝜑 is ⊤ in at least one row of its truth table and ⊥ in at least one row of its truth table/ 𝜑 obtains in at least one possible world and doesn't obtain in at least one possible world
𝜑 is a theorem of L1= : 𝜑 is a tautology derived from the axioms of L1=.
Based on the above truth tables:
¬¬𝜑 ↔︎ 𝜑
𝜑 → (𝜓 → 𝜑)
𝜑 → 𝜑
(𝜑 & ¬𝜑) → 𝜓
¬(𝜑 & ¬𝜑)
(𝜑 & 𝜓) → 𝜑
(𝜑 & 𝜓) → 𝜓
(𝜑 → 𝜓) → (¬𝜓 → ¬𝜑)
𝜑 ∨ ¬𝜑
¬(𝜑 ⊻ 𝜑)
𝜑 → (𝜑 ∨ 𝜓)
𝜑 → (𝜓 ∨ 𝜑)
⊢(𝜑 → 𝜓) , ⊢𝜑 ⇒ ⊢𝜓
#1 - #12 are all tautologies. One can check this using truth tables. #13 is based on the semantics of L1= and the first row of the truth table of the conditional.
However, for practicality, I will use the following set of axioms for L1=. These are also tautologies and the above axioms can all be derived from this set as theorems when the logical conjunction (&), inclusive disjunction (∨), exclusive disjunction (⊻) are defined:
(𝜑 & 𝜓) ≝ ¬(𝜑 → ¬𝜓)
(𝜑 ∨ 𝜓) ≝ (¬𝜑 → 𝜓)
(𝜑 ⊻ 𝜓) ≝ ¬(𝜑 ↔︎ 𝜓)
These definitions are chosen so because the formulae used for the defining have the same truth table as the formula that they each defines. For example, the truth table of ¬(𝜑 → ¬𝜓) is the same as the truth table of (𝜑 & 𝜓):
(⊤ → ⊤) : ⊤ , (⊤ → ¬⊤) : ⊥ , ¬(⊤ → ¬⊤) : ⊤
(⊤ → ⊥) : ⊥ , (⊤ → ¬⊥) : ⊤ , ¬(⊤ → ¬⊥) : ⊥
(⊥ → ⊤) : ⊤ , (⊥ → ¬⊤) : ⊤ , ¬(⊥ → ¬⊤) : ⊥
(⊥ → ⊥) : ⊤ , (⊥ → ¬⊥) : ⊤ , ¬(⊥ → ¬⊥) : ⊥
Ax. 1 'Simplification': ⊢ 𝜑 → (𝜓 → 𝜑)
Ax. 2 'Frege': ⊢ [𝜑 → (𝜓 → 𝜒)] → [(𝜑 → 𝜓) → (𝜑 → 𝜒)]
Ax. 3 'Transposition': ⊢ (¬𝜑 → ¬𝜓) → (𝜓 → 𝜑)
Ax. 4 (inference rule) 'Modus ponens': ⊢(𝜑 → 𝜓) , ⊢𝜑 ⇒ ⊢𝜓 (based on first row of the truth table of →)
Ax. 5 (inference rule) 'Definitional soundness 1': ⊢(𝜑 ≝ 𝜓) & ⊢𝜒[𝜓] ⇒ ⊢𝜒[𝜑/𝜓] provided that 𝜑 doesn't occur within the wff 𝜓 and 𝜓 doesn't occur within 𝜑
Ax. 6 (inference rule) 'Definitional soundness 2': ⊢(𝜑 ≝ 𝜓) & ⊢𝜒[𝜑] ⇒ ⊢𝜒[𝜓/𝜑] provided that 𝜑 doesn't occur within the wff 𝜓 and 𝜓 doesn't occur within 𝜑
Based on 1.1, 1.6, 1.7, and 1.8, these are the axioms of first-order predicate logic.
Ax. 7 (inference rule) 'Generalization': ⊢𝜑 ⇒ ⊢(∀𝜁)𝜑(𝜁), provided that 𝜑 is either an axiom or a theorem of L1+ZF and is derived from an axiom or a theorem of L1+ZF; 'if 𝜑 is a theorem, then it is true of anything'
Note: the 𝜑 cannot be '☐𝜓', otherwise the derived formula wouldn't be well-formed
Ax. 8 'Quantified conditional ': ⊢ (∀𝜁)[𝜑(𝜁) → 𝜓(𝜁)] → [(∀𝜁)𝜑(𝜁) → (∀𝜁)𝜓(𝜁)] 'if, for each object 𝜁, if 𝜑 being true of that object implies 𝜓 also being true of that object, then, 𝜑 being true for everything implies 𝜓 being true for everything'
Ax. 9 'Distinctness': ⊢(𝜑(𝛽, 𝛾...) → (∀[𝜁/𝛼])𝜑(𝛽, 𝛾...)] provided that 𝛼 doesn't occur in the wff 𝜑
This axiom has a side condition. If any proof utilizes this axiom, the side condition becomes part of the proven theorem.
'if 𝛼 doesn't occur in 𝜑, then generalizing on 𝛼 alone doesn't affect the truth of 𝜑' (this axiom is trivial)
Ax. 10 'Existence': ⊢ ¬(∀𝜁)¬(𝜁 = 𝛼) 'it is not the case that everything is not identical to an individual object, in other words, 'something exists'
Ax. 11 'Identity': ⊢ (𝛼 = 𝛽) → [(𝛼 = 𝛾) → (𝛽 = 𝛾)]
Ax. 12 'Left identity for binary relations': ⊢ (𝛼 = 𝛽) → (𝚷2(𝛼, 𝛾) → 𝚷2(𝛽, 𝛾))
Ax. 13 'Right Identity for binary relations': ⊢ (𝛼 = 𝛽) → (𝚷2(𝛾, 𝛼) → 𝚷2(𝛾, 𝛽)
Based on 1.2 and 1.6, these are part of Zermelo-Fraenkel set theory without the Axiom of Choice
Ax. 14 'Extensionality': ⊢ (∀𝜁)[(𝜁 ∈ 𝚷) ↔︎ (𝜁 ∈ 𝛀)] → (𝚷 = 𝛀) ' the identity of a set is determined only by its member(s)
Ax. 15 'Replacement': ⊢ (∀x)(∃𝚷)(∀y){ [(∀𝚷)𝜑 → (y = 𝚷)] → (∃𝚷)(∀y)[(y ∈ 𝚷)) ↔︎ (∃x)((x ∈ 𝛀) & (∀𝚷)𝜑)] } 'the image of a set under a function is also a set'
Ax. 16 'Union': ⊢ (∀𝚷)(∃𝛀)(∀𝜁){(∃𝚺)[(𝜁 ∈ 𝚺) & (𝚺 ∈ 𝚷)] → [𝜁 ∈ 𝛀)} 'for any set 𝚷, there is a set (𝛀) that contains every member 𝜁 of the members (𝚺) of 𝚷'
Ax. 17 'Regularity': ⊢(∃𝜁)(𝜁 ∈ 𝚷) → (∃𝜀)[(𝜀 ∈ 𝚷) & ([𝜀 ∩ 𝚷] = ∅)] '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': ⊢ (∀𝚷)(∃𝛀)(∀𝚺){(∀𝜁)[(𝜁 ∈ 𝚺) → (𝜁 ∈ 𝚷)] → (𝚺 ∈ 𝛀)} 'for any set 𝚷, there is a set (𝛀) that only contains every subset (𝚺) of 𝚷'
Ax. 19 'Infinity': ⊢ (∃𝚷){[∅ ∈ 𝚷] & (∀𝛀)[(𝛀 ∈ 𝚷) → (∃𝚺)([𝚺 ∈ 𝚷] & (∀𝜁){ (𝜁 ∈ 𝚺) ↔ [(𝜁 ∈ 𝛀) ∨ (𝜁 = 𝛀)] } ) ) 'there is a set 𝚷 that contains the empty set and, for every subset (𝛀) of 𝚷, there is another subset (𝚺) of 𝚷 whose members are all either also contained in 𝛀 or identical to 𝛀',
Remarks: Since the empty set is a subset of 𝚷, there is another subset ('1') of 𝚷 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 𝚷, whose members are either just '1' or all members of '1', or both, and so on. Thus, 𝚷 is an infinite set. This axiom is for positing the various 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' ⊢ (Ⅎ𝜁)[¬(∀𝜁)𝜑(𝜁)] 'All occurrences of 𝜁 in ¬(∀𝜁)𝜑(𝜁) is bounded by a quantifier (in this case, ∀)' (analogous to Ax. 10 of Metamath)
Ax. 21 'Universal quantifier commutation' ⊢ (∀𝜁)(∀𝜀)𝜑 → (∀𝜀)(∀𝜁)𝜑 'the ∀ quantifiers binding to two different variables can be switched'
Ax. 22 'Substitution' ⊢ (𝜁 = 𝜀) → [(∀𝜀)𝜑 → (∀𝜁)[(𝜁 = 𝜀) → 𝜑]] 'if 𝜁 is identical to 𝜀, then, if every 𝜀 is 𝜑 then everything identical to 𝜀 is also 𝜑'
Ax. 23 'Quantified distinctness' ⊢ ¬(𝜁 = 𝛼) → [(𝛼 = 𝛽) → (∀𝜁)(𝛼 = 𝛽)] 'if 𝜁 is distinct from 𝛼, then quantifying over the identity of 𝛼 with 𝛽 doesn't affect its truth' (analogous to Ax. 7)
Ax. 24 (inference rule) 'Deduction' [(𝚪 & 𝜑) ⊢ 𝜓] ⇒ ⊢[𝚪 ⊢ (𝜑 → 𝜓)] , where 𝚪 is a (possibly empty) set of wffs, (usually proven as the 'Deduction Theorem', this states that if 𝜓 was proven from 𝜑 with the set of premises 𝚪, then the conditional 𝜑 → 𝜓 also logically follows from 𝚪) (this axiom, along with modus ponens, means that logical consequence and the conditional imply each other)
Based on 1.3 and 1.5, these are the axioms of alethic modal logic.
Ax. 25 (inference rule) 'Necessitation': ⊢𝜑 ⇒ ⊢☐𝜑 , provided that 𝜑 is a either a non-modal axiom or a non-modal theorem of L1+ZF 'if 𝜑 is a theorem, then 𝜑 necessarily obtains'
Note: 𝜑 cannot be ☐𝜑, otherwise the derived formula would be not well-formed.
Ax. 26 'Kripke': ⊢☐(𝜑 → 𝜓) → (☐𝜑 → ☐𝜓) 'if necessarily, if 𝜑 obtains then 𝜓 also obtains, then, if 𝜑 necessarily obtains then 𝜓 also necessarily obtains'
Ax. 27 'Necessity': ⊢ ☐𝜑 → 𝜑 'if 𝜑 necessarily obtains, then 𝜑 obtains'