P. 4 of Theorem List - Linear Logic Proof Explorer

Home	Linear Logic Proof Explorer Theorem List (p. 4 of 4)	< Previous  Wrap >
		Mirrors  >  Metamath Home Page  >  LLPE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Linear Logic Proof Explorer - 301-335   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	weqtru 301	Truth judgement.
wff ⊨ P
Syntax	weqfal 302	Falsity judgement.
wff ⊭ P
Definition	df-eqtru 303	A shorthand way of saying that a church-encoded value is true. I would totally use this as a new typecode, so I could prove statements with ⊨ instead of ⊦, but it turns out that adds needless complexity (and mmj2 doesn't like it).
⊦ (P = True ⧟ ⊨ P)
Definition	df-eqfal 304	A shorthand way of saying that a church-encoded value is false. Note that this is not the opposite of df-eqtru 303 (although they do exclude each other), since there are many more things an expression could equal.
⊦ (P = False ⧟ ⊭ P)
Theorem	dfeqtru1i 305	Introduce ⊨.
⊦ P = True    ⇒   ⊦ ⊨ P
Theorem	dfeqtru2i 306	Eliminate ⊨.
⊦ ⊨ P    ⇒   ⊦ P = True
Theorem	tru 307	True is true. Who'd've thunk it.
⊦ ⊨ True
Syntax	nlimpl 308	Function representing logical implication.
nilad Impl
Syntax	nland 309	Function representing logical conjunction.
nilad And
Syntax	nlor 310	Function representing logical disjunction.
nilad Or
Syntax	nlnot 311	Function representing logical negation.
nilad Not
Syntax	nliff 312	Function representing logical biconditional.
nilad Iff
Definition	df-limpl 313*	Church-encoding of logical conjunction.
⊦ Impl = λaλb(baTrue)
Definition	df-land 314*	Church-encoding of logical conjunction.
⊦ And = λaλb(baFalse)
Definition	df-lor 315*	Church-encoding of logical disjunction.
⊦ Or = λaλb(Trueab)
Definition	df-lnot 316*	Church-encoding of logical negation.
⊦ Not = λaλxλy(yax)
Definition	df-liff 317*	Church-encoding of logical biconditional.
⊦ Iff = λaλb(ba(Not' b))
1.5  Quantifiers and equality Oh boy. This is unexplored territory for me. I'm just going to copy all the FOL axioms from set.mm and hope that works. I'm preeety sure that all those are valid theorems in linear logic; I'm just not sure whether they're sufficient. I think they are. Probably.
1.5.1  Axioms for predicate logic with equality
Syntax	wal 318	Universal quantifier. Characterized by ax-genOLD 323, ax-almd 324, ax-dis 325, ax-ex 326, ax-negf 330, ax-alcom 331.
wff ∀x𝜑
Syntax	wex 319	Existential quantifier. Defined by df-ex 334.
wff ∃x𝜑
Syntax	wnf 320	Not-free predicate. Defined by df-nf 335.
wff Ⅎx𝜑
Theorem	weqOLD 321	Equality. Charactrized by ax-ex 326, ax-sub 332, ax-aleq 333, ax-eqeu 327.
⊦ (𝜑 ⊸ 𝜑)
Syntax	wel 322	Set element predicate. For the purposes of predicate logic, it's just an arbitrary operator.
wff x ∈ y
Axiom	ax-genOLD 323	Axiom of generalization. Universal quantifiers can be freely added to the start of an expression.
⊦ 𝜑    ⇒   ⊦ ∀x𝜑
Axiom	ax-almd 324	Quantified multiplicative disjunction. This "distributes" a quantifier over linear implication.
⊦ (∀x(𝜑 ⊸ 𝜓) ⊸ (∀x𝜑 ⊸ ∀x𝜓))
Axiom	ax-dis 325*	Distinctness principle. When the value of 𝜑 is independent of x, a quantifier can be added.
⊦ (𝜑 ⊸ ∀x𝜑)
Axiom	ax-ex 326	Axiom of existence. This axiom is secretly two useful axioms in one. It states that any y has an x that is equal to it. It also states that there exists something equal to itself, when y is substituted for x.
⊦ ~ ∀x~ x = y
Axiom	ax-eqeu 327	Equality is Euclidean. Combined with ax-ex 326, this implies that equality is symmetric and transitive.
⊦ (x = y ⊸ (x = z ⊸ y = z))
Axiom	ax-eleq1 328	Left equality for binary predicate. This consumes the equality.
⊦ (x = y ⊸ (x ∈ z ⊸ y ∈ z))
Axiom	ax-eleq2 329	Right equality for binary predicate. This consumes the equality.
⊦ (x = y ⊸ (z ∈ x ⊸ z ∈ y))
1.5.2  Auxiliary axioms for predicate logic with equality
Axiom	ax-negf 330	Axiom of quantified negation.
⊦ (~ ∀x𝜑 ⊸ ∀x~ ∀x𝜑)
Axiom	ax-alcom 331	Quantifier commutation.
⊦ (∀x∀y𝜑 ⊸ ∀y∀x𝜑)
Axiom	ax-sub 332	Axiom of variable substitution.
⊦ (x = y ⊸ (∀y𝜑 ⊸ ∀x(x = y ⊸ 𝜑)))
Axiom	ax-aleq 333	Quantified equality.
⊦ (~ x = y ⊸ (y = z ⊸ ∀x y = z))
Definition	df-ex 334	Definition of existential quantifier. Dual of ∀.
⊦ (∃x𝜑 ⧟ ~ ∀x~ 𝜑)
Definition	df-nf 335	Definition of not-free predicate.
⊦ (Ⅎx𝜑 ⧟ (~ 𝜑 ⊸ ∀x𝜑))

< Previous  Wrap >