P. 2 of Theorem List - Linear Logic Proof Explorer

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

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

Type	Label	Description
Statement
Theorem	lbtri 101	Linear biconditional is transitive. Inference for lbtr 128.
⊦ (𝜑 ⧟ 𝜓)    &   ⊦ (𝜓 ⧟ 𝜒)    ⇒   ⊦ (𝜑 ⧟ 𝜒)
Theorem	lbsymd 102	Linear biconditional is symmetric. Deduction for lbsym 127.
⊦ (𝜑 ⊸ (𝜓 ⧟ 𝜒))    ⇒   ⊦ (𝜑 ⊸ (𝜒 ⧟ 𝜓))
1.1.5  Operator properties and duals All operators in linear logic have a dual. The dual operator is the same as its corresponding operator but negated, similar to 𝜑 ∧ 𝜓 ↔ ¬ (¬ 𝜑 ∨ ¬ 𝜓) in classical logic. Here we will characterize the dual operators. Also, now that we finally have the underpinnings for linear logic completely set up, we can finally establish the properties of the operators alongside their duals. This will make it much easier to do more interesting proofs.
1.1.5.1  Multiplicatives revisited
Syntax	wone 103	One, the unit of ⊗. Defined by df-one 104.
wff 1
Definition	df-one 104	One is the dual of Bottom.
⊦ (1 ⧟ ~ ⊥)
Syntax	wmc 105	Times, multiplicative conjunction. Defined by df-mc 106.
wff (𝜑 ⊗ 𝜓)
Definition	df-mc 106	Times is the dual of Par.
⊦ ((𝜑 ⊗ 𝜓) ⧟ ~ (~ 𝜑 ⅋ ~ 𝜓))
Theorem	dn 107	Double negation elimination and introduction.
⊦ (𝜑 ⧟ ~ ~ 𝜑)
Theorem	mdco 108	⅋ is commutative.
⊦ ((𝜑 ⅋ 𝜓) ⊸ (𝜓 ⅋ 𝜑))
Theorem	mdcob 109	⅋ is commutative. Biconditional version of mdco 108.
⊦ ((𝜑 ⅋ 𝜓) ⧟ (𝜓 ⅋ 𝜑))
Theorem	mdas 110	⅋ is associative.
⊦ (((𝜑 ⅋ 𝜓) ⅋ 𝜒) ⊸ (𝜑 ⅋ (𝜓 ⅋ 𝜒)))
Theorem	mdasrNEW 111	⅋ is associative. Reverse of mdas 110.
⊦ ((𝜑 ⅋ (𝜓 ⅋ 𝜒)) ⊸ ((𝜑 ⅋ 𝜓) ⅋ 𝜒))
Theorem	mdasb 112
⊦ (((𝜑 ⅋ 𝜓) ⅋ 𝜒) ⧟ (𝜑 ⅋ (𝜓 ⅋ 𝜒)))
Theorem	md1 113	⊥ is the unit of ⅋ (left side).
⊦ (𝜑 ⧟ (⊥ ⅋ 𝜑))
Theorem	md2 114	⊥ is the unit of ⅋ (right side).
⊦ (𝜑 ⧟ (𝜑 ⅋ ⊥))
Theorem	mcco 115	⊗ is commutative. TODO extract double negation theorems, licon 94 alternate forms
⊦ ((𝜑 ⊗ 𝜓) ⊸ (𝜓 ⊗ 𝜑))
Theorem	mccob 116	⊗ is commutative. Biconditional version of mcco 115.
⊦ ((𝜑 ⊗ 𝜓) ⧟ (𝜓 ⊗ 𝜑))
Theorem	mcas 117	⊗ is associative.
⊦ (((𝜑 ⊗ 𝜓) ⊗ 𝜒) ⊸ (𝜓 ⊗ (𝜓 ⊗ 𝜒)))
Theorem	mcasb 118	⊗ is associative.
⊦ (((𝜑 ⊗ 𝜓) ⊗ 𝜒) ⧟ (𝜓 ⊗ (𝜓 ⊗ 𝜒)))
Theorem	mc1 119	1 is the unit of ⊗ (left side).
⊦ (𝜑 ⧟ (1 ⊗ 𝜑))
Theorem	mc2 120	1 is the unit of ⊗ (right side).
⊦ (𝜑 ⧟ (𝜑 ⊗ 1))
Theorem	one 121	1. It's very true, but is it as true as ⊤ (itop 146, top 147)? Discuss.
⊦ 1
Theorem	init 122	Creation of 𝜑 and its dual from 1. Dual of initr 123.
⊦ (1 ⊸ (𝜑 ⅋ ~ 𝜑))
Theorem	initr 123	Annihilation of 𝜑 and its dual into ⊥. Dual of init 122.
⊦ ((𝜑 ⊗ ~ 𝜑) ⊸ ⊥)
Theorem	mcmd 124	Association of ⊗ into ⅋. The converse of this rule does not hold. This theorem is its own dual: By flipping the ⊸ around and swapping ⊗ and ⅋, you end up with the same theorem.
⊦ ((𝜑 ⊗ (𝜓 ⅋ 𝜒)) ⊸ ((𝜑 ⊗ 𝜓) ⅋ 𝜒))
Theorem	merge 125	Combine ⅋ statements by a single term.
⊦ (((𝜑 ⅋ 𝜓) ⊗ (𝜒 ⅋ 𝜃)) ⊸ ((𝜑 ⅋ (𝜓 ⊗ 𝜒)) ⅋ 𝜃))
Theorem	lbeu 126	Linear biconditional is Euclidean.
⊦ (((𝜑 ⧟ 𝜓) ⊗ (𝜑 ⧟ 𝜒)) ⊸ (𝜓 ⧟ 𝜒))
Theorem	lbsym 127	Linear biconditional is symmetric.
⊦ ((𝜑 ⧟ 𝜓) ⊸ (𝜓 ⧟ 𝜑))
Theorem	lbtr 128	Linear biconditional is transitive.
⊦ (((𝜑 ⧟ 𝜓) ⊗ (𝜓 ⧟ 𝜒)) ⊸ (𝜑 ⧟ 𝜒))
1.1.5.2  Additives revisited
Syntax	wzero 129	Zero, the unit of ⊕. Defined by df-zero 130.
wff 0
Definition	df-zero 130	Zero is the dual of Top.
⊦ (0 ⧟ ~ ⊤)
Syntax	wad 131	Plus, additive disjunction. Defined by df-ad 132.
wff (𝜑 ⊕ 𝜓)
Definition	df-ad 132	Plus is the dual of With.
⊦ ((𝜑 ⊕ 𝜓) ⧟ ~ (~ 𝜑 & ~ 𝜓))
Theorem	adcob 133	⊕ is commutative.
⊦ ((𝜑 ⊕ 𝜓) ⧟ (𝜓 ⊕ 𝜑))
Theorem	adasb 134	⊕ is associative.
⊦ (((𝜑 ⊕ 𝜓) ⊕ 𝜒) ⧟ (𝜓 ⊕ (𝜓 ⊕ 𝜒)))
Theorem	ad1 135	0 is the unit of ⊕ (left side).
⊦ (𝜑 ⧟ (0 ⊕ 𝜑))
Theorem	ad2 136	0 is the unit of ⊕ (right side).
⊦ (𝜑 ⧟ (𝜑 ⊕ 0))
Theorem	accob 137	& is commutative.
⊦ ((𝜑 & 𝜓) ⧟ (𝜓 & 𝜑))
Theorem	acasb 138	& is associative.
⊦ (((𝜑 & 𝜓) & 𝜒) ⧟ (𝜓 & (𝜓 & 𝜒)))
Theorem	ac1 139	⊤ is the unit of & (left side).
⊦ (𝜑 ⧟ (⊤ & 𝜑))
Theorem	ac2 140	⊤ is the unit of & (right side).
⊦ (𝜑 ⧟ (𝜑 & ⊤))
Theorem	eac1 141	Select the left side of &. Dual of iad1 143.
⊦ ((𝜑 & 𝜓) ⊸ 𝜑)
Theorem	eac2 142	Select the left side of &. Dual of iad2 144.
⊦ ((𝜑 & 𝜓) ⊸ 𝜓)
Theorem	iad1 143	Introduce a ⊕ (left side). Dual of eac1 141.
⊦ (𝜑 ⊸ (𝜑 ⊕ 𝜓))
Theorem	iad2 144	Introduce a ⊕ (right side). Dual of eac2 142.
⊦ (𝜓 ⊸ (𝜑 ⊕ 𝜓))
Theorem	ezer 145	From 0, infer all.
⊦ (0 ⊸ 𝜑)
Theorem	itop 146	Everything can be turned into ⊤.
⊦ (𝜑 ⊸ ⊤)
Theorem	top 147	Hey, that's ⊤. A direct consequence of itop 146.
⊦ ⊤
1.1.5.3  Exponentials revisited
Syntax	wpe 148	"Of course", positive exponential. Defined by df-pe 149.
wff ! 𝜑
Definition	df-pe 149	"Of course" is the dual of "Why not".
⊦ (! 𝜑 ⧟ ~ ? ~ 𝜑)
Theorem	weak 150	Create ? 𝜑 from ⊥.
⊦ (⊥ ⊸ ? 𝜑)
Theorem	dupr 151	Unduplicate ? 𝜑.
⊦ ((? 𝜑 ⊗ ? 𝜑) ⊸ ? 𝜑)
Theorem	dig 152	Dig out a ? from ⅋.
⊦ (? (? 𝜑 ⊗ ? 𝜑) ⊸ (? 𝜑 ⊗ ? 𝜑))
Theorem	dig1 153	Dig out a ? from a single term.
⊦ (? ? 𝜑 ⊸ ? 𝜑)
Theorem	ine 154	Promote 𝜑 to ? 𝜑.
⊦ (𝜑 ⊸ ? 𝜑)
Theorem	weakr 155	Destroy ! 𝜑.
⊦ (! 𝜑 ⊸ 1)
Theorem	dup 156	Duplicate ! 𝜑.
⊦ (! 𝜑 ⊸ (! 𝜑 ⊗ ! 𝜑))
Theorem	bury 157	Bury ⅋ with !.
⊦ ((! 𝜑 ⊗ ! 𝜑) ⊸ ! (! 𝜑 ⊗ ! 𝜑))
Theorem	bury1 158	Bury a single term with !.
⊦ (! 𝜑 ⊸ ! ! 𝜑)
Theorem	epe 159	Demote ! 𝜑 to 𝜑.
⊦ (! 𝜑 ⊸ 𝜑)
Theorem	peone 160	! 1. It's like 1 but even more.
⊦ ! 1
Theorem	petop 161	! ⊤. It's like ⊤ but even more.
⊦ ! ⊤
Theorem	ipe 162	Introduce positive exponential at the top level. TODO: Extract lemmas for double negation, intro ? 𝜑, and more. Also get the proof back because it exploded
⊦ 𝜑    ⇒   ⊦ ! 𝜑
1.1.6  Miscellaneous theorems Here are some old uncategorized theorems. They need to be placed into an appropriate section and renamed.
Theorem	ionei 163	Insert One into Times.
⊦ 𝜑    ⇒   ⊦ (𝜑 ⊗ 1)
Theorem	eonei 164	Remove One from Times.
⊦ (𝜑 ⊗ 1)    ⇒   ⊦ 𝜑
Theorem	mcasd 165	Times is associative.
⊦ (𝜑 ⅋ ((𝜓 ⊗ 𝜒) ⊗ 𝜃))    ⇒   ⊦ (𝜑 ⅋ (𝜓 ⊗ (𝜒 ⊗ 𝜃)))
Theorem	mcasrd 166	Times is associative.
⊦ (𝜑 ⅋ (𝜓 ⊗ (𝜒 ⊗ 𝜃)))    ⇒   ⊦ (𝜑 ⅋ ((𝜓 ⊗ 𝜒) ⊗ 𝜃))
Theorem	mccod 167	Times is commutative.
⊦ (𝜑 ⅋ (𝜓 ⊗ 𝜒))    ⇒   ⊦ (𝜑 ⅋ (𝜒 ⊗ 𝜓))
Theorem	mcm1s 168	Times is monotone in its first argument.
⊦ (𝜑 ⊸ 𝜒)    ⇒   ⊦ ((𝜑 ⊗ 𝜓) ⊸ (𝜒 ⊗ 𝜓))
Theorem	mcm2s 169	Times is monotone in its second argument.
⊦ (𝜓 ⊸ 𝜒)    ⇒   ⊦ ((𝜑 ⊗ 𝜓) ⊸ (𝜑 ⊗ 𝜒))
Theorem	izerOLD 170	Insert Zero into Plus.
⊦ 𝜑    ⇒   ⊦ (𝜑 ⊕ 0)
Theorem	ezerOLD 171	Remove Zero from Plus.
⊦ (𝜑 ⊕ 0)    ⇒   ⊦ 𝜑
Theorem	adas 172	Plus is associative.
⊦ (𝜑 ⅋ ((𝜓 ⊕ 𝜒) ⊕ 𝜃))    ⇒   ⊦ (𝜑 ⅋ (𝜓 ⊕ (𝜒 ⊕ 𝜃)))
Theorem	adasr 173	Plus is associative.
⊦ (𝜑 ⅋ (𝜓 ⊕ (𝜒 ⊕ 𝜃)))    ⇒   ⊦ (𝜑 ⅋ ((𝜓 ⊕ 𝜒) ⊕ 𝜃))
Theorem	adco 174	Plus is commutative.
⊦ (𝜑 ⅋ (𝜓 ⊕ 𝜒))    ⇒   ⊦ (𝜑 ⅋ (𝜒 ⊕ 𝜓))
Theorem	adm1s 175	Plus is monotone in its first argument.
⊦ (𝜑 ⊸ 𝜒)    ⇒   ⊦ ((𝜑 ⊕ 𝜓) ⊸ (𝜒 ⊕ 𝜓))
Theorem	adm2s 176	Plus is monotone in its second argument.
⊦ (𝜓 ⊸ 𝜒)    ⇒   ⊦ ((𝜑 ⊕ 𝜓) ⊸ (𝜑 ⊕ 𝜒))
Theorem	pems 177	"Of Course" is monotone.
⊦ (𝜑 ⊸ 𝜓)    ⇒   ⊦ (! 𝜑 ⊸ ! 𝜓)
Theorem	abs1 178	Absorption of Plus into With. Together with abs2 179, this shows the additive operators form a lattice.
⊦ ((𝜑 ⊕ (𝜑 & 𝜓)) ⧟ 𝜑)
Theorem	abs2 179	Absorption into Plus. Together with abs1 178, this shows the additive operators form a lattice.
⊦ ((𝜑 & (𝜑 ⊕ 𝜓)) ⧟ 𝜑)
1.2  Intuitionistic logic There exists a nice conversion between statements in intuitionistic logic to statements in linear logic. Basically, just throw a bunch of ! exponentials everywhere and you're good to go. Classical logic can then be recovered using the magic of double negatives. This conversion relies on the fact that all statements on the "top level", meaning all axioms, proofs, and hypotheses, have an implicit ! as shown by ax-ipe 49. The rules of classical and intuitionistic logic dictate that all expressions can be duplicated in this manner, which is accomplished by filling the subexpressions with lots of !. In this section, all of the axioms of intuitionistic logic used in the Metamath iset.mm database are proven. This means that linear logic could feasibly be used as a background logic for set theory. I wonder what interesting consequences would come from this?
Syntax	wim 180	Logical implication. Defined by df-im 181.
wff (𝜑 → 𝜓)
Definition	df-im 181	Definition of →. It's ⊸ but with some ! splashed in for good measure. Note that only 𝜑 needs the exponential. When this statement is beneath a ! or at the top level, this is equivalent to both sides having the exponential, because of
⊦ ((𝜑 → 𝜓) ⧟ (! 𝜑 ⊸ 𝜓))
Syntax	wand 182	Logical conjunction. Defined by df-and 183.
wff (𝜑 ∧ 𝜓)
Definition	df-and 183	Definition of ∧. It's & but with some ! splashed in for good measure.
⊦ ((𝜑 ∧ 𝜓) ⧟ (! 𝜑 & ! 𝜓))
Syntax	wor 184	Logical disjunction. Defined by df-or 185.
wff (𝜑 ∨ 𝜓)
Definition	df-or 185	Definition of ∨. It's ⊕ but with some ! splashed in for good measure.
⊦ ((𝜑 ∨ 𝜓) ⧟ (! 𝜑 ⊕ ! 𝜓))
Syntax	wnot 186	Logical negation. Defined by df-not 187.
wff ¬ 𝜑
Definition	df-not 187	Definition of ¬. It's ~ but with some ! splashed in for good measure.
⊦ (¬ 𝜑 ⧟ ~ ! 𝜑)
Syntax	wbi 188	Logical biconditional. Defined by df-bi 189.
wff (𝜑 ↔ 𝜓)
Definition	df-bi 189	Definition of ↔, in terms of the other logical connectives.
⊦ ((𝜑 ↔ 𝜓) ⧟ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))
Theorem	simp 190	Principle of simplification. Allows discarding an unneeded antecedent. This is not possible with linear implication, since such a move would be non-linear; the ! exponentials in the definition of the logical implication operator allow 𝜓 to be discarded. Axiom 1 in the Metamath iset.mm database.
⊦ (𝜑 → (𝜓 → 𝜑))
Theorem	frege 191	Axiom 2 in the Metamath iset.mm database. This uses the other property of the positive exponential, which is that it can be duplicated.
⊦ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Theorem	mp 192	Good ol' classic modus ponendo ponens. Doesn't it feel weird to have this be a theorem rather than an axiom?
⊦ 𝜑    &   ⊦ (𝜑 → 𝜓)    ⇒   ⊦ 𝜓
Theorem	ea1 193	Left 'and' elimination. Axiom ia1 in iset.mm.
⊦ ((𝜑 ∧ 𝜓) → 𝜑)
Theorem	ea2 194	Right 'and' elimination. Axiom ia2 in iset.mm.
⊦ ((𝜑 ∧ 𝜓) → 𝜓)
Theorem	ia 195	'And' introduction. Axiom ia3 in iset.mm.
⊦ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
Theorem	or 196	'Or' elimination, and its converse. Axiom io in iset.mm.
⊦ (((𝜑 ∨ 𝜓) → 𝜒) ↔ ((𝜑 → 𝜒) ∧ (𝜓 → 𝜒)))
Theorem	inot 197	'Not' introduction. Axiom in1 in iset.mm.
⊦ ((𝜑 → ¬ 𝜑) → ¬ 𝜑)
Theorem	enot 198	'Not' elimination. Axiom in2 in iset.mm.
⊦ (¬ 𝜑 → (𝜑 → 𝜓))
Theorem	simpi 199	Inference using simplification. Adds an unneeded antecedent. Inference for simp 190.
⊦ 𝜑    ⇒   ⊦ (𝜓 → 𝜑)
Theorem	fregei 200	Inference using transposition. Inference for frege 191.
⊦ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊦ ((𝜑 → 𝜓) → (𝜑 → 𝜒))