P. 1 of Theorem List - Linear Logic Proof Explorer

Home	Linear Logic Proof Explorer Theorem List (p. 1 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 - 1-100   *Has distinct variable group(s)

Type	Label	Description
Statement
PART 1  Hilbert-style axiomatisation of Linear Logic This is an implementation of Girard's linear logic based on Axioms and Models of Linear Logic by Wim H. Hesselink. Thanks to the dual nature of linear logic, many of the operators are redundant. Only the ⅋, &, ?, and ~ operators and the units ⊥ and ⊤ are needed to construct any expression. The only problem is that to write the definitions of the composite operators, the linear biconditional ⧟ is needed, which in turn depends on ~, ⅋, and &. Because of this, any proofs that use the composite operators are presented after all the axioms and definitions.
1.1  Basic stuff Here the operators ⊥, ⅋, ⊤, &, ?, and ~ are defined. Later, the duals 1, ⊕, 0, ⊗, ! are defined, plus the implication operators ⊸, ⧟, and the intuitionistic operators ∧, ∨, ¬, →, and ↔. Due to the way defenitions work in Metamath (i.e. they don't), my first priority is to get the linear biconditional ⧟ working so that it can be used to define the other operators. Unfortunately, the definition of the linear biconditional depends on ⅋, &, and ~, so those need to be defined first. Proofs are generally most useful in the syllogism form (𝜑 ⊸ 𝜓) → (𝜑 ⊸ 𝜒), so I'll avoid proving stuff here only to prove it again once ⊸ is defined. Since linear implication is not available, inferences will be presented in deduction form (𝜑 ⅋ 𝜓) ∧ (𝜑 ⅋ 𝜒) → (𝜑 ⅋ 𝜃). This is equivalent to (! 𝜓 ⊗ ! 𝜒) ⊸ 𝜃. This allows proofs to be used with the cut rule.
1.1.1  Multiplicatives There are two multiplicative binary connectives: ⊗ and ⅋. In the resource interpretation, these correspond to treating the resources involved in a parallel manner. Here we characterize ⅋, and df-mc 106 will define ⊗ as its dual.
Syntax	wbot 1	Bottom, the unit of ⅋. In the resource interpretation, this represents an impossibility. Characterized by ax-ibot 4 and ax-ebot 5.
wff ⊥
Syntax	wmd 2	Par, multiplicative disjunction. In the resource interpretation, this represents resources that are to be used in parallel. Characterized by ax-init 7, ax-cut 6, ax-mdco 8, ax-mdas 9.
wff (𝜑 ⅋ 𝜓)
Syntax	wneg 3	Linear negation. For any statement 𝜑, ~ 𝜑 is its dual. In the resource interpretation, this represents demand for something (sort of kind of). Combining 𝜑 and ~ 𝜑 yields ⊥.
wff ~ 𝜑
Axiom	ax-ibot 4	Add a ⊥. Inverse of ax-ebot 5.
⊦ 𝜑    ⇒   ⊦ (⊥ ⅋ 𝜑)
Axiom	ax-ebot 5	Remove a ⊥. Inverse of ax-ibot 4.
⊦ (⊥ ⅋ 𝜑)    ⇒   ⊦ 𝜑
Axiom	ax-cut 6	The cut rule is akin to syllogism in classical logic. It allows ~ 𝜑 ⅋ 𝜓 to act like an implication, so that an 𝜑 can be removed and traded for a 𝜓.
⊦ (𝜑 ⅋ 𝜓)    &   ⊦ (~ 𝜓 ⅋ 𝜒)    ⇒   ⊦ (𝜑 ⅋ 𝜒)
Axiom	ax-init 7	The init rule. This innocent-looking rule looks similar to the Law of Excluded Middle in classical logic, but don't be fooled. This allows us to turn any deduction into its dual by simply performing operations on the ~ 𝜑 side and flipping it around to get the reverse implication. This is analogous to using modus tollens in classical logic, but it's especially useful in linear logic because it allows each operator to be defined as its dual with all of the deductions negated and backwards.
⊦ (~ 𝜑 ⅋ 𝜑)
Axiom	ax-mdco 8	⅋ is commutative.
⊦ (~ (𝜑 ⅋ 𝜓) ⅋ (𝜓 ⅋ 𝜑))
Axiom	ax-mdas 9	⅋ is associative.
⊦ (~ ((𝜑 ⅋ 𝜓) ⅋ 𝜒) ⅋ (𝜑 ⅋ (𝜓 ⅋ 𝜒)))
Theorem	cut1 10	Modus ponens like inference.
⊦ 𝜑    &   ⊦ (~ 𝜑 ⅋ 𝜓)    ⇒   ⊦ 𝜓
Theorem	mdcod 11	⅋ is commutative. Deduction form of ax-mdco 8.
⊦ (𝜃 ⅋ (𝜑 ⅋ 𝜓))    ⇒   ⊦ (𝜃 ⅋ (𝜓 ⅋ 𝜑))
Theorem	mdcoi 12	⅋ is commutative. Inference form of ax-mdco 8.
⊦ (𝜑 ⅋ 𝜓)    ⇒   ⊦ (𝜓 ⅋ 𝜑)
Theorem	mdasd 13	⅋ is associative. Deduction form of ax-mdas 9.
⊦ (𝜃 ⅋ ((𝜑 ⅋ 𝜓) ⅋ 𝜒))    ⇒   ⊦ (𝜃 ⅋ (𝜑 ⅋ (𝜓 ⅋ 𝜒)))
Theorem	mdasi 14	⅋ is associative. Inference form of ax-mdas 9.
⊦ ((𝜑 ⅋ 𝜓) ⅋ 𝜒)    ⇒   ⊦ (𝜑 ⅋ (𝜓 ⅋ 𝜒))
Theorem	mdasr 15	⅋ is associative. Reverse of ax-mdas 9.
⊦ (~ (𝜑 ⅋ (𝜓 ⅋ 𝜒)) ⅋ ((𝜑 ⅋ 𝜓) ⅋ 𝜒))
Theorem	mdasrd 16	⅋ is associative. Deduction form of mdasr 15.
⊦ (𝜃 ⅋ (𝜑 ⅋ (𝜓 ⅋ 𝜒)))    ⇒   ⊦ (𝜃 ⅋ ((𝜑 ⅋ 𝜓) ⅋ 𝜒))
Theorem	mdasri 17	⅋ is associative. Inference form of mdasrd 16.
⊦ (𝜑 ⅋ (𝜓 ⅋ 𝜒))    ⇒   ⊦ ((𝜑 ⅋ 𝜓) ⅋ 𝜒)
Theorem	ibotr 18	Add a ⊥, right hand side. See ax-ibot 4.
⊦ 𝜑    ⇒   ⊦ (𝜑 ⅋ ⊥)
Theorem	ebotr 19	Remove a ⊥, right hand side. See ax-ebot 5.
⊦ (𝜑 ⅋ ⊥)    ⇒   ⊦ 𝜑
Theorem	nebot 20	Infer ~ ⊥ (secretly 1).
⊦ ~ ⊥
Theorem	cutneg 21	Negated version of ax-cut 6.
⊦ (𝜑 ⅋ ~ 𝜓)    &   ⊦ (𝜓 ⅋ 𝜒)    ⇒   ⊦ (𝜑 ⅋ 𝜒)
Theorem	cutf 22	Left-hand version of ax-cut 6.
⊦ (𝜓 ⅋ 𝜑)    &   ⊦ (~ 𝜓 ⅋ 𝜒)    ⇒   ⊦ (𝜒 ⅋ 𝜑)
Theorem	dnid 23	Double negation introduction.
⊦ (𝜑 ⅋ 𝜓)    ⇒   ⊦ (𝜑 ⅋ ~ ~ 𝜓)
Theorem	dned 24	Double negation elimination.
⊦ (𝜑 ⅋ ~ ~ 𝜓)    ⇒   ⊦ (𝜑 ⅋ 𝜓)
Theorem	dni1 25	Double negation introduction, left hand side.
⊦ (𝜑 ⅋ 𝜓)    ⇒   ⊦ (~ ~ 𝜑 ⅋ 𝜓)
Theorem	dne1 26	Double negation elimination, left hand side.
⊦ (~ ~ 𝜑 ⅋ 𝜓)    ⇒   ⊦ (𝜑 ⅋ 𝜓)
Theorem	inenebot 27	Add a ~ ~ ⊥. See ax-ibot 4. This is useful for dealing with deductions where the antecedent is negated.
⊦ 𝜑    ⇒   ⊦ (~ ~ ⊥ ⅋ 𝜑)
Theorem	enenebot 28	Remove a ~ ~ ⊥. Inverse of inenebot 27.
⊦ (~ ~ ⊥ ⅋ 𝜑)    ⇒   ⊦ 𝜑
1.1.2  Additives There are two additive binary connectives: & and ⊕. These relate to treating the involved expressions independently. Here we characterize &, and df-ad 132 will define ⊕ as its dual.
Syntax	wtop 29	Top, the unit of &. In the resource interpretation, this represents an unknown collection of objects. Characterized by ax-top 31.
wff ⊤
Syntax	wac 30	With, additive conjunction. In the resource interpretation, this represents a choice between two resources. Characterized by ax-iac 32, ax-eac1 33, ax-eac2 34.
wff (𝜑 & 𝜓)
Axiom	ax-top 31	Anything can turn into ⊤.
⊦ (~ 𝜑 ⅋ ⊤)
Axiom	ax-iac 32	& introduction rule.
⊦ (~ 𝜑 ⅋ 𝜓)    &   ⊦ (~ 𝜑 ⅋ 𝜒)    ⇒   ⊦ (~ 𝜑 ⅋ (𝜓 & 𝜒))
Axiom	ax-eac1 33	& elimination rule, left hand side.
⊦ (~ 𝜑 ⅋ (𝜓 & 𝜒))    ⇒   ⊦ (~ 𝜑 ⅋ 𝜓)
Axiom	ax-eac2 34	& elimination rule, right hand side.
⊦ (~ 𝜑 ⅋ (𝜓 & 𝜒))    ⇒   ⊦ (~ 𝜑 ⅋ 𝜒)
Theorem	iac 35	& introduction rule. ax-iac 32 has a negation for some reason, this one doesn't.
⊦ (𝜑 ⅋ 𝜓)    &   ⊦ (𝜑 ⅋ 𝜒)    ⇒   ⊦ (𝜑 ⅋ (𝜓 & 𝜒))
Theorem	iaci 36	& introduction rule. Inference form of ax-iac 32.
⊦ 𝜑    &   ⊦ 𝜓    ⇒   ⊦ (𝜑 & 𝜓)
Theorem	eac1d 37	& elimination rule, left hand side. ax-eac1 33 has a negation for some reason, this one doesn't.
⊦ (𝜑 ⅋ (𝜓 & 𝜒))    ⇒   ⊦ (𝜑 ⅋ 𝜓)
Theorem	eac1i 38	& elimination rule, left hand side. Inference form of ax-eac1 33.
⊦ (𝜑 & 𝜓)    ⇒   ⊦ 𝜑
Theorem	eac2d 39	& elimination rule, right hand side. ax-eac2 34 has a negation for some reason, this one doesn't.
⊦ (𝜑 ⅋ (𝜓 & 𝜒))    ⇒   ⊦ (𝜑 ⅋ 𝜒)
Theorem	eac2i 40	& elimination rule, right hand side. Inference form of ax-eac2 34.
⊦ (𝜑 & 𝜓)    ⇒   ⊦ 𝜓
Theorem	itopi 41	Insert Top into With. Inverse of etopi 42.
⊦ 𝜑    ⇒   ⊦ (𝜑 & ⊤)
Theorem	etopi 42	Remove Top from With. This is, of course, just a special case of ax-eac1 33.
⊦ (𝜑 & ⊤)    ⇒   ⊦ 𝜑
Theorem	acco 43	& is commutative.
⊦ (𝜑 ⅋ (𝜓 & 𝜒))    ⇒   ⊦ (𝜑 ⅋ (𝜒 & 𝜓))
Theorem	acas 44	& is associative.
⊦ (𝜑 ⅋ ((𝜓 & 𝜒) & 𝜃))    ⇒   ⊦ (𝜑 ⅋ (𝜓 & (𝜒 & 𝜃)))
Theorem	acasr 45	& is associative. Reverse of acas 44.
⊦ (𝜑 ⅋ (𝜓 & (𝜒 & 𝜃)))    ⇒   ⊦ (𝜑 ⅋ ((𝜓 & 𝜒) & 𝜃))
Theorem	dismdac 46	⅋ distributes over &.
⊦ (𝜑 ⅋ (𝜓 ⅋ (𝜒 & 𝜃)))    ⇒   ⊦ (𝜑 ⅋ ((𝜓 ⅋ 𝜒) & (𝜓 ⅋ 𝜃)))
Theorem	extmdac 47	⅋ extracts out of &. Converse of dismdac 46.
⊦ (𝜑 ⅋ ((𝜓 ⅋ 𝜒) & (𝜓 ⅋ 𝜃)))    ⇒   ⊦ (𝜑 ⅋ (𝜓 ⅋ (𝜒 & 𝜃)))
1.1.3  Exponentials There are two exponential connectives: ? and !. These allow expressions to be duplicated and deleted. Here we characterize ?, and df-pe 149 will define ! as its dual.
Syntax	wne 48	"Why not", negative exponential. Characterized by ax-ipe 49, ax-epe 50, ax-weak 51, ax-contr 52, ax-pemc 53, ax-dig 54.
wff ? 𝜑
Axiom	ax-ipe 49	Add a ? (secretly a !). Inverse of ax-epe 50.
⊦ (~ 𝜑 ⅋ ? 𝜓)    ⇒   ⊦ (~ ? 𝜑 ⅋ ? 𝜓)
Axiom	ax-epe 50	Remove a ? (secretly a !). Inverse of ax-ipe 49.
⊦ (~ ? 𝜑 ⅋ ? 𝜓)    ⇒   ⊦ (~ 𝜑 ⅋ ? 𝜓)
Axiom	ax-weak 51	? 𝜑 can be added into any statement.
⊦ (~ ⊥ ⅋ ? 𝜑)
Axiom	ax-contr 52	? 𝜑 can be contracted.
⊦ (~ (? 𝜑 ⅋ ? 𝜑) ⅋ ? 𝜑)
Axiom	ax-pemc 53	! 1. This is needed to let ax-ipe 49 and ax-epe 50 work on single items.
⊦ ~ ? ⊥
Axiom	ax-dig 54	If all the elements of a multiplicative disjunction have ?, then ? can be removed from that disjunction.
⊦ (~ ? (? 𝜑 ⅋ ? 𝜓) ⅋ (? 𝜑 ⅋ ? 𝜓))
1.1.4  Implication Yay, implication! The linear implication operator 𝜑 ⊸ 𝜓 reads as, "Given a 𝜑, I can exchange it for a 𝜓." This is closely related to the logical implication → which can be interpreted as, "Given a proof of 𝜑, I can prove 𝜓." The important difference is that the linear implication and the antecedent are both consumed by this action. The linear biconditional can work either way; the choice is given to you by the & in its definition. The linear biconditional is used to write all definitions, except itself (df-lb 56).
Syntax	wlb 55	Linear biconditional, defined by df-lb 56. This is the operator used for definitions, so its definition will be a little unusual...
wff (𝜑 ⧟ 𝜓)
Definition	df-lb 56	Definition of linear biconditional. Since the linear implication has not been defined, this is a mouthfull. The good news is, once the properties of the linear biconditional are proven, it will be much easier to express other definitions. See dflb 93 for a cleaner form of the definition.
⊦ ((~ (𝜑 ⧟ 𝜓) ⅋ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑))) & (~ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑)) ⅋ (𝜑 ⧟ 𝜓)))
Theorem	lb1d 57	Forward deduction using ⧟.
⊦ (𝜑 ⅋ 𝜓)    &   ⊦ (𝜓 ⧟ 𝜒)    ⇒   ⊦ (𝜑 ⅋ 𝜒)
Theorem	lb2d 58	Reverse deduction using ⧟.
⊦ (𝜑 ⅋ 𝜒)    &   ⊦ (𝜓 ⧟ 𝜒)    ⇒   ⊦ (𝜑 ⅋ 𝜓)
Theorem	lb1i 59	Forward inference using ⧟.
⊦ 𝜑    &   ⊦ (𝜑 ⧟ 𝜓)    ⇒   ⊦ 𝜓
Theorem	lb2i 60	Reverse inference using ⧟.
⊦ 𝜓    &   ⊦ (𝜑 ⧟ 𝜓)    ⇒   ⊦ 𝜑
Syntax	wli 61	Linear implication, defined by df-li 62. Now that linear implication exists, we can finally put things in syllogism form from here on.
wff (𝜑 ⊸ 𝜓)
Definition	df-li 62	Definition of linear implication.
⊦ ((𝜑 ⊸ 𝜓) ⧟ (~ 𝜑 ⅋ 𝜓))
Theorem	dfli1 63	Convert from linear implication.
⊦ (𝜑 ⅋ (𝜓 ⊸ 𝜒))    ⇒   ⊦ (𝜑 ⅋ (~ 𝜓 ⅋ 𝜒))
Theorem	dfli2 64	Convert to linear implication.
⊦ (𝜑 ⅋ (~ 𝜓 ⅋ 𝜒))    ⇒   ⊦ (𝜑 ⅋ (𝜓 ⊸ 𝜒))
Theorem	dfli1i 65	Convert from linear implication. Inference for dfli1 63.
⊦ (𝜓 ⊸ 𝜒)    ⇒   ⊦ (~ 𝜓 ⅋ 𝜒)
Theorem	dfli2i 66	Convert to linear implication. Inference for dfli2 64.
⊦ (~ 𝜓 ⅋ 𝜒)    ⇒   ⊦ (𝜓 ⊸ 𝜒)
Theorem	lb1s 67	Forward syllogism using ⧟.
⊦ (𝜑 ⊸ 𝜓)    &   ⊦ (𝜓 ⧟ 𝜒)    ⇒   ⊦ (𝜑 ⊸ 𝜒)
Theorem	lb2s 68	Reverse syllogism using ⧟.
⊦ (𝜑 ⊸ 𝜒)    &   ⊦ (𝜓 ⧟ 𝜒)    ⇒   ⊦ (𝜑 ⊸ 𝜓)
Theorem	mdm2 69	Par is monotone in its second argument.
⊦ (𝜃 ⅋ (𝜑 ⅋ 𝜓))    &   ⊦ (𝜓 ⊸ 𝜒)    ⇒   ⊦ (𝜃 ⅋ (𝜑 ⅋ 𝜒))
Theorem	mdm1 70	Par is monotone in its first argument.
⊦ (𝜃 ⅋ (𝜑 ⅋ 𝜓))    &   ⊦ (𝜑 ⊸ 𝜒)    ⇒   ⊦ (𝜃 ⅋ (𝜒 ⅋ 𝜓))
Theorem	mdm1i 71	Par is monotone in its first argument. Inference form of mdm1 70.
⊦ (𝜑 ⅋ 𝜓)    &   ⊦ (𝜑 ⊸ 𝜒)    ⇒   ⊦ (𝜒 ⅋ 𝜓)
Theorem	mdm2i 72	Par is monotone in its second argument. Inference form of mdm2 69. Essentially ax-cut 6 using linear implication.
⊦ (𝜑 ⅋ 𝜓)    &   ⊦ (𝜓 ⊸ 𝜒)    ⇒   ⊦ (𝜑 ⅋ 𝜒)
Theorem	mdm1s 73	Par is monotone in its first argument. Syllogism form of mdm1 70.
⊦ (𝜑 ⊸ 𝜒)    ⇒   ⊦ ((𝜑 ⅋ 𝜓) ⊸ (𝜒 ⅋ 𝜓))
Theorem	mdm2s 74	Par is monotone in its second argument. Syllogism form of mdm2 69.
⊦ (𝜓 ⊸ 𝜒)    ⇒   ⊦ ((𝜑 ⅋ 𝜓) ⊸ (𝜑 ⅋ 𝜒))
Theorem	syl 75	Syllogism using linear implication.
⊦ (𝜑 ⊸ 𝜓)    &   ⊦ (𝜓 ⊸ 𝜒)    ⇒   ⊦ (𝜑 ⊸ 𝜒)
Theorem	lmp 76	Modus ponens like inference using linear implication.
⊦ 𝜑    &   ⊦ (𝜑 ⊸ 𝜓)    ⇒   ⊦ 𝜓
Theorem	id 77	Identity rule for linear implication. Syllogism form of ax-init 7.
⊦ (𝜑 ⊸ 𝜑)
Theorem	dnis 78	Double negation introduction. Syllogism form of dnid 23.
⊦ (𝜑 ⊸ ~ ~ 𝜑)
Theorem	dnes 79	Double negation elimination. Syllogism form of dned 24.
⊦ (~ ~ 𝜑 ⊸ 𝜑)
Theorem	acm1 80	With is monotone in its first argument.
⊦ (𝜃 ⅋ (𝜑 & 𝜓))    &   ⊦ (𝜑 ⊸ 𝜒)    ⇒   ⊦ (𝜃 ⅋ (𝜒 & 𝜓))
Theorem	acm2 81	With is monotone in its second argument.
⊦ (𝜃 ⅋ (𝜑 & 𝜓))    &   ⊦ (𝜓 ⊸ 𝜒)    ⇒   ⊦ (𝜃 ⅋ (𝜑 & 𝜒))
Theorem	acm1i 82	With is monotone in its first argument. Inference form of acm1 80.
⊦ (𝜑 & 𝜓)    &   ⊦ (𝜑 ⊸ 𝜒)    ⇒   ⊦ (𝜒 & 𝜓)
Theorem	acm2i 83	With is monotone in its second argument. Inference form of acm2 81.
⊦ (𝜑 & 𝜓)    &   ⊦ (𝜓 ⊸ 𝜒)    ⇒   ⊦ (𝜑 & 𝜒)
Theorem	acm1s 84	With is monotone in its first argument. Syllogism form of acm1 80.
⊦ (𝜑 ⊸ 𝜒)    ⇒   ⊦ ((𝜑 & 𝜓) ⊸ (𝜒 & 𝜓))
Theorem	acm2s 85	With is monotone in its second argument. Syllogism form of acm2 81.
⊦ (𝜓 ⊸ 𝜒)    ⇒   ⊦ ((𝜑 & 𝜓) ⊸ (𝜑 & 𝜒))
Theorem	nems 86	"Why not" is monotone.
⊦ (𝜑 ⊸ 𝜓)    ⇒   ⊦ (? 𝜑 ⊸ ? 𝜓)
Theorem	lbi1s 87	Extract forward implication from biconditional. Syllogism form of lb1i 59.
⊦ ((𝜑 ⧟ 𝜓) ⊸ (𝜑 ⊸ 𝜓))
Theorem	lbi2s 88	Extract reverse implication from biconditional. Syllogism form of lb2i 60.
⊦ ((𝜑 ⧟ 𝜓) ⊸ (𝜓 ⊸ 𝜑))
Theorem	lbi1 89	Extract forward implication from biconditional. Alternate form of lb1i 59.
⊦ (𝜑 ⧟ 𝜓)    ⇒   ⊦ (𝜑 ⊸ 𝜓)
Theorem	lbi2 90	Extract reverse implication from biconditional. Alternate form of lb2i 60.
⊦ (𝜑 ⧟ 𝜓)    ⇒   ⊦ (𝜓 ⊸ 𝜑)
Theorem	dflb1s 91	Forward implication of biconditional definition.
⊦ ((𝜑 ⧟ 𝜓) ⊸ ((𝜑 ⊸ 𝜓) & (𝜓 ⊸ 𝜑)))
Theorem	dflb2s 92	Reverse implication of biconditional definition.
⊦ (((𝜑 ⊸ 𝜓) & (𝜓 ⊸ 𝜑)) ⊸ (𝜑 ⧟ 𝜓))
Theorem	dflb 93	Nicer definition of biconditional. Uses ⧟ and ⊸.
⊦ ((𝜑 ⧟ 𝜓) ⧟ ((𝜑 ⊸ 𝜓) & (𝜓 ⊸ 𝜑)))
Theorem	licon 94	Contrapositive rule for linear implication. This follows quite neatly from df-li 62.
⊦ ((𝜑 ⊸ 𝜓) ⊸ (~ 𝜓 ⊸ ~ 𝜑))
Theorem	licond 95	Deduction form of licon 94.
⊦ (𝜒 ⅋ (𝜑 ⊸ 𝜓))    ⇒   ⊦ (𝜒 ⅋ (~ 𝜓 ⊸ ~ 𝜑))
Theorem	ilb 96	Construct a biconditional from its forward and reverse implications.
⊦ (𝜑 ⊸ 𝜓)    &   ⊦ (𝜓 ⊸ 𝜑)    ⇒   ⊦ (𝜑 ⧟ 𝜓)
Theorem	ilbd 97	Construct a biconditional from its forward and reverse implications.
⊦ (𝜑 ⊸ (𝜓 ⊸ 𝜒))    &   ⊦ (𝜑 ⊸ (𝜒 ⊸ 𝜓))    ⇒   ⊦ (𝜑 ⊸ (𝜓 ⧟ 𝜒))
Theorem	lbrf 98	Linear biconditional is reflexive. This could be thought of as "both directions" of id 77.
⊦ (𝜑 ⧟ 𝜑)
Theorem	lbeui 99	Linear biconditional is Euclidean. Inference for lbeu 126.
⊦ (𝜑 ⧟ 𝜓)    &   ⊦ (𝜑 ⧟ 𝜒)    ⇒   ⊦ (𝜓 ⧟ 𝜒)
Theorem	lbsymi 100	Linear biconditional is symmetric. Inference for lbsym 127.
⊦ (𝜑 ⧟ 𝜓)    ⇒   ⊦ (𝜓 ⧟ 𝜑)