This page details a formal language ('L1+ZF') to be used in this blog in order to enable symbolization and proofs.
Well-formed formula (wff): A formula that is part of a formal language such that meaning can be assigned to it according to the semantics of that language
Also simply called 'formula of L' (where L is a specific formal language, in this case L1+ZF)
Variable: a symbol that can serve as a placeholder for anything that is not a variable
Metavariable: a symbol that can serve as a placeholder for any variables
The italic, lowercase Greek letters with or without the subscript n: 𝛼, 𝛽, 𝛾, 𝛼n are metavariables that can serve as a placeholder for any individual constants (a, b, c, d, a1, a2, a3, c11, etc.).
The italic, lowercase Greek letters, with or without the subscript n, 𝜑, 𝜓, 𝜒 are metavariables that can serve as a placeholder for any wffs.
The bold, uppercase Greek letter with the superscript n, 𝚷n is a metavariable that can serve as a placeholder for any n-place predicate variables (A𝛼, B(𝛼, 𝛽), P𝛼, etc.).
The bold, uppercase Greek letters, 𝚷, 𝛀, 𝚺 are metavariables that can serve as a placeholder for any set variables (A, B, C, etc.).
The italic, lowercase Greek letter 𝜁, 𝜀 and 𝜅 are metavariables that can serve as a placeholder for any variables x, y, and z, and the metavariables 𝚷, 𝛀, 𝚺.
The uppercase Latin letters A, B, C, P, etc. are variables that can serve as a placeholder for any wffs.
The lowercase Latin letters x, y, z, and w are variables that can serve as a placeholder for any individual constants.
The bold, uppercase Latin letters, A, B, C, S, etc. are variables that can serve as a placeholder for any sets.
The uppercase Latin letters joined by an individual constant: Aa, Ba, Cs, Sh, etc, or joined by individual constants inside parentheses: A(a, b), B(a, b, c), etc. are variables that can serve as a placeholder for any n-place predicates (such as 'is a mother' (1-place) and 'is a mother of' (2-place)).
The lowercase Latin letters, with or without numerical subscripts, a, b, c, d, a1, a2, a3, c11, etc. (except x, y, and z) are individual constants that can serve as a placeholder for any individual object.
(, ) (parentheses)
[, ] (brackets)
{, } (curly brackets)
⟨, ⟩ (angle bracket)
, (comma)
/ ('substitutes for', uniform substitution)
Unary operators
¬ (negation, 'NOT')
☐ (necessity, 'necessarily')
⃟ (possibility, 'possibly')
Binary operators
→ (material conditional, 'IMPLIES', 'if...then')
& (conjunction, AND)
∨ (inclusive disjunction, OR)
⊻ (exclusive disjunction, XOR)
↔︎ (material biconditional, XNOR, 'only when', 'only in case', 'if and only if', 'iff')
= (absolute identity, equality, 'is identical to', 'is equal to')
≠ (inequality, 'not identical to', 'not equal to')
n-ary operator
∧ (conjunction, AND)
⋎ (inclusive disjunction, OR)
⩒ (exclusive disjunction, XOR)
Variable-binding operators
∀ (universal quantifier, 'for all', 'for every', 'for any')
∃ (existential quantifier, 'there exists')
Ⅎ (boundedness operator, 'is a bounded variable', the Ⅎ is from 'not-free')
⊤ ('true')
⊥ ('false')
⊢ ('is deducible from', 'is provable from')
⇒ ('then')
≝ (definition, 'is defined as')
⊨ (semantic consequence, 'validates', 'is a semantic consequence of')
∈ (set membership, 'is an element(s) of')
∉ ('is not an element(s) of')
⊆ ('is a subset of or equal to')
⊇ ('is a superset of or equal to')
⊂ ('is a subset of', 'is a proper subset of')
⊃ ('is a superset of', 'is a proper superset of')
∩ (n-ary set intersection)
∪ (n-ary set union)
∅ (the empty set)
The syntax of L1+ZF is given recursively as followed:
If 𝛼, 𝛽, and 𝛾 are any individual constants of L1+ZF, and 𝚷n, 𝛀n, and 𝚺n are any n-place predicates of L1+ZF, then if n ≥ 1, then 𝚷𝛼, 𝚷𝛽, 𝚷𝛾, 𝚷n(𝛼n, 𝛼n-1, ... 𝛼2, 𝛼1) are wffs.
𝜑, 𝜓, and 𝜒 are wffs.
A, B, C ... P are wffs.
If 𝜑 is a wff, then (¬𝜑) is a wff.
If 𝜑 and 𝜓 are wffs, then (𝜑 → 𝜓) is a wff.
If 𝜑 is a wff that is not (☐𝜓), and 𝜁, 𝜀 and 𝜅 are one of the variables x, y, z, w, 𝚷, 𝛀, 𝚺, then [(∀𝜁)𝜑], [(∀𝜀)𝜑], [(∀𝜅)𝜑], [(∀𝜁 ∈ 𝜀)𝜑], and [(∀*𝜁 ∈ 𝜀)𝜑] are wffs.
If 𝜑 and 𝜓 are wffs, then (𝜑 ⊢ 𝜓) is a wff.
If 𝜑 and 𝜓 are wffs, then (𝜑 ⇒ 𝜓) is a wff.
If 𝛼 and 𝛽 are any individual constants of L1+ZF, and 𝜁 is one of the variables x, y, z, w, 𝚷, 𝛀, 𝚺, then (𝛼 ∈ 𝜁) and (𝛽 ∈ 𝜁) are wffs.
If 𝛼 and 𝛽 are any individual constants of L1+ZF, then (𝛼 ∈ 𝛽) is a wff.
If 𝜁 and 𝜀 are one of the variables x, y, z, w, 𝚷, 𝛀, 𝚺, then (𝜁 ∈ 𝜀) is a wff.
If 𝛼 and 𝛽 are any individual constants of L1+ZF, and if 𝜁 is one of the variables x, y, z, w, 𝚷, 𝛀, 𝚺, then (𝛼 = 𝜁) and (𝛽 = 𝜁) are wffs.
If 𝛼 and 𝛽 are any individual constants of L1+ZF, then (𝛼 = 𝛽) is a wff.
If 𝜁, 𝜀, and 𝜅 are one of the variables x, y, z, w, 𝚷, 𝛀, 𝚺, then (𝜁 = 𝜀) and (𝜀 = 𝜅) are wffs.
{𝜁 | 𝜑} is a wff.
If 𝜑 and 𝜓 are wffs, then (𝜑 ≝ 𝜓) is a wff.
If 𝜑 and 𝜓 are wffs, then (𝜑 ∈ 𝜓) is a wff.
If 𝜑 is a wff and if 𝜁 and 𝜀 are one of the variables x, y, z, w, 𝚷, 𝛀, 𝚺, then 𝜑[𝜁/𝜀] is a wff.
If 𝛼 is any individual constants of L1+ZF, and if 𝜁 is one of the variables x, y, z, w, 𝚷, 𝛀, 𝚺, then 𝜑[𝛼/𝜁] and 𝜑[𝜁/𝛼] are wffs.
If 𝜁 and 𝜀 are one of the variables x, y, z, and w, and 𝚷n, 𝛀n, and 𝚺n are any n-place predicates of L1+ZF, then if n ≥ 1, then 𝚷𝜁, 𝚷𝜀, 𝛀𝜁, 𝛀𝜀, 𝚺𝜁, and 𝚺𝜀 are wffs.
{𝜑}, {𝜑, 𝜓}, and {𝜑, 𝜓, 𝜒, ...} are wffs.
If 𝜑 is a wff that is not (☐𝜓), then (☐𝜑) is a wff.
Nothing else is a wff.
These definitions are for abbreviating certain wffs. These abbreviations don't allow us to prove any new theorem in the system that isn't already provable without the added definition. In a proof, it allows one to substitute a wff completely with the wff on the other side of the 'defined as' sign ≝, provided that a wff on one side is not part of the wff on the other side. Note that, without this restriction, definitions would be different from a mere abbreviation. If one abbreviates the name 'John' using just the letter 'J', one cannot substitute the first letter (J) of 'John' with 'John' in order to derive 'Johnohn'. Since we want a definer wff to be substitutable by a defined wff, we need an analogous restriction on substitutability to preserve definitions as mere abbreviations.
Since real-world concepts are attached to the symbols being defined, a justification is given for each.
(𝜑 & 𝜓) ≝ ¬(𝜑 → ¬𝜓) [truth table, see Axioms]
(𝜑 ∨ 𝜓) ≝ (¬𝜑 → 𝜓) [truth table, see Axioms]
(𝜑 ⊻ 𝜓) ≝ ¬(𝜑 ↔︎ 𝜓) [truth table, see Axioms]
(𝜑 ↔︎ 𝜓) ≝ [(𝜑 → 𝜓) & (𝜓 → 𝜑)] [usage in math]
(∃𝜁)𝜑 ≝ ¬(∀𝜁)¬𝜑 ['there is a P' = 'it is not the case that everything isn't P']
(𝛼 ≠ 𝛽) ≝ ¬(𝛼 = 𝛽) ['unequal' = 'not equal']
(𝚷 ∉ 𝛀) ≝ ¬(𝚷 ∈ 𝛀) [usage in math]
(𝛼 ∉ 𝛀) ≝ ¬(𝛼 ∈ 𝛀) [same]
(𝚷 ⊆ 𝛀) ≝ (∀𝜁)[(𝜁 ∈ 𝚷) → (𝜁 ∈ 𝛀)] [same]
(𝚷 ⊇ 𝛀) ≝ (∀𝜁)[(𝜁 ∈ 𝛀) → (𝜁 ∈ 𝚷)] [same]
(𝚷 ⊂ 𝛀) ≝ [(∀𝜁)[(𝜁 ∈ 𝚷) → (𝜁 ∈ 𝛀)] & (𝚷 ≠ 𝛀)] [same]
(𝚷 ⊃ 𝛀) ≝ [(∀𝜁)[(𝜁 ∈ 𝛀) → (𝜁 ∈ 𝚷)] & (𝚷 ≠ 𝛀)] [same]
(𝜁 ∈ {𝜀 | 𝜑}) ≝ 𝜑[𝜁/𝜀] (def. used in Metamath)
∅ ≝ {x | ¬(x = x)} (same)
(𝜑1 ∧ 𝜑2 ∧ 𝜑3 ∧ ... ∧ 𝜑n) ≝ [𝜑n & (𝜑n-1 & (𝜑n-2 & (... & (𝜑2 & 𝜑1))))] [iterated conjunction]
(𝜑1 ⋎ 𝜑2 ⋎ 𝜑3 ⋎ ... ⋎ 𝜑n) ≝ [𝜑n ∨ (𝜑n-1 ∨ (𝜑n-2 ∨ (... ∨ (𝜑2 ∨ 𝜑1))))] [iterated disjunction]
(𝜑1 ⩒ 𝜑2 ⩒ 𝜑3 ⩒ ... ⩒ 𝜑n) ≝ {[𝜑n ∨ (𝜑n-1 ∨ (𝜑n-2 ∨ (... ∨ (𝜑2 ∨ 𝜑1))))] & (𝚽 = {𝜑1, 𝜑2, 𝜑3, ... , 𝜑n}) & (∀x)([(x ∈ 𝚽) ∧ (y ∈ 𝚽) ∧ (x ≠ y)] → ¬(x & y)) [iterated exclusive disjunction only allows exactly one of the disjuncts to be true]
(∀𝜁 ∈ 𝜀)𝜑 ≝ (∀𝜁)[(𝜁 ∈ 𝜀) → 𝜑] (def. of restricted universal quantification used in Metamath)
(∃𝜁 ∈ 𝜀)𝜑 ≝ (∃𝜁)[(𝜁 ∈ 𝜀) & 𝜑] (def. of restricted existential quantification used in Metamath)
(Ⅎ𝜁)𝜑 ≝ (∀𝜁)(𝜑 → (∀𝜁)𝜑) (def. of boundedness of 𝜁 in 𝜑 used in Metamath)
⃟𝜑 ≝ ¬☐¬𝜑 (possibly 𝜑 = not necessarily not 𝜑)
𝜑[𝛼/𝜁] ≝ {[(𝜁 = 𝛼) → 𝜑] & (∃𝜁)[(𝜁 = 𝛼) & 𝜑]} [def. of substitution used in Metamath]
𝜑[𝜁/𝛼] ≝ {[(𝜁 = 𝛼) → 𝜑] & (∃𝜁)[(𝜁 = 𝛼) & 𝜑]} [same]
𝜑[𝜁/𝜀] ≝ {[(𝜁 = 𝜀) → 𝜑] & (∃𝜀)[(𝜁 = 𝜀) & 𝜑]} [same]
(∀*𝜁 ∈ 𝜀)𝜑 ≝ [(∀𝜁)[(𝜁 ∈ 𝜀) → 𝜑] & (∃𝜁)(𝜁 ∈ 𝜀)] (def. of natural restricted quantification)
W𝜁 ≝ [(𝜁 ∈ W) & (∀𝜀)[(𝜀 ≠ W) → (𝜁 ∉ 𝜀)]] 'the property of being a possible world is being a member of the set of worlds and not being a member of any other set'
☐𝜑 ≝ (∀𝜁)[W𝜁 → (∃𝜀)[(𝜀 ∈ 𝜁) & (𝜀 ↔︎ 𝜑)]] [alternative definition of necessity = for all 𝜁, if 𝜁 is a possible world, then there is a subset of 𝜁 that implies 𝜑]
◇𝜑 ≝ (∃𝜁)[W𝜁 & (∃𝜀)[(𝜀 ∈ 𝜁) & (𝜀 ↔︎ 𝜑)]] [alternate definition of possibility = there is a world with a subset that implies 𝜑]
A first-order, varying-domain Kripke model M is a quintuple ⟨W, R, D, Q, I⟩, where W is the nonempty set of possible worlds w, R is a binary relation between these worlds, D is a nonempty set (called the ‘domain of discourse’) of individual objects, Q is a function that takes in a world and gives out a subset of D, and I is the interpretation function that
takes in an n-place predicate and gives out a set of n-tuples of members of Q(w),
takes in an individual constant and gives out a member of Q(w).
𝜇 is a value-assignment function which assign its input (variables x, y, or z) a member of D.
'M, 𝜇, w ⊨ 𝜑' ≝ 'LSoA 𝜑 is a subset of w, in M under assignment 𝜇'
'M, 𝜇, w ⊭ 𝜑' ≝ 'LSoA 𝜑 is not a subset of w, in M under assignment 𝜇'
M, 𝜇, w ⊨ ¬𝜑 only in case M, 𝜇, w ⊭ 𝜑
M, 𝜇, w ⊨ (𝜑 → 𝜓) only in cases M, 𝜇, w ⊭ 𝜑 or M, 𝜇, w ⊨ 𝜓, or both
M, 𝜇, w ⊨ (𝜑 & 𝜓) only in case both M, 𝜇, w ⊨ 𝜑 and M, 𝜇, w ⊨ 𝜓
M, 𝜇, w ⊨ (𝜑 ∨ 𝜓) only in cases either M, 𝜇, w ⊨ 𝜑 or M, 𝜇, w ⊨ 𝜓, or both
M, 𝜇, w ⊨ (𝜑 ⊻ 𝜓) only in cases either M, 𝜇, w ⊨ 𝜑 or M, 𝜇, w ⊨ 𝜓, but not both
M, 𝜇, w ⊨ (𝜑 ↔︎ 𝜓) only in cases either, M, 𝜇, w ⊨ 𝜑 and M, 𝜇, w ⊨ 𝜓, or, M, 𝜇, w ⊭ 𝜑 and M, 𝜇, w ⊭ 𝜓, but not both
M, 𝜇, w ⊨ 𝚷n𝛼1𝛼2…𝛼n only in case ⟨I(𝛼1), I(𝛼2),..., I(𝛼n)⟩ ∈ I(𝚷n)
M, 𝜇, w ⊨ (𝛼 = 𝛽) only in case I(𝛼) is identical to I(𝛽)
M, 𝜇, w ⊨ (∀𝜁)𝜑 only in case, for all individuals 𝛼 contained in Q(w), (M, 𝜇, w ⊨ 𝜑) when 𝛼 substitutes for 𝜁
M, 𝜇, w ⊨ (∃𝜁)𝜑 only in case, there is at least one individual 𝛼 contained in Q(w) such that (M, 𝜇, w ⊨ 𝜑) when 𝛼 substitutes for 𝜁
M, 𝜇, w ⊨ ☐𝜑 only in case, for every possible world w in W, (M, 𝜇, w ⊨ 𝜑)
M, 𝜇, w ⊨ ⃟𝜑 only in case, in at least one possible world w in W, (M, 𝜇, w ⊨ 𝜑)