Wikiproofs - Recent changes [en]

User:Kingdon

Kingdon — Sat, 04 Sep 2010 19:36:05 GMT

finished a lot of the arithmetic todos here

← Older revision		Revision as of 19:36, 4 September 2010
Line 32:		Line 32:
	=== Theorems ===		=== Theorems ===
	Sample theorems from Hirst & Hirst:		Sample theorems from Hirst & Hirst:
-	~~4. Strict inequality is transitive: x < y → (y < z → x < z)~~
-	~~5. Inequality is preserved by addition: x ≤ y → x + z ≤ y + z (one direction of leadd1)~~
-	~~6. Strict inequality is preserved by addition: x < y → x + z < y + z~~
	7. Inequality is preserved by multiplication: x ≤ y → x · z ≤ y · z (lemul2, commuted)		7. Inequality is preserved by multiplication: x ≤ y → x · z ≤ y · z (lemul2, commuted)
	8. Strict inequality is preserved by nonzero multiplication:		8. Strict inequality is preserved by nonzero multiplication:
	z ≠ 0 → (x < y → x · z < y · z)		z ≠ 0 → (x < y → x · z < y · z)
-	~~9. Inequalities can be added: (w ≤ x ∧ y ≤ z) → w + y ≤ x + z~~
	10. Inequalities can be multiplied: (w ≤ x ∧ y ≤ z) → w · y ≤ x · z		10. Inequalities can be multiplied: (w ≤ x ∧ y ≤ z) → w · y ≤ x · z

	No zero divisors: a · b = 0 → (a = 0 ∨ b = 0)		No zero divisors: a · b = 0 → (a = 0 ∨ b = 0)
-
-	~~Some definitions:~~
-
-	* x < y ↔ x ≤ y ∧ x ≠ y
-	* x > y ↔ y < x
-	* x ≥ y ↔ y ≤ x

	More theorems:		More theorems:

	* x ≠ 0 ↔ x > 0		* x ≠ 0 ↔ x > 0
-
-	~~We'll show that it has the [[w:Total order\|expected properties of an order]].~~
-	* If a ≤ b and b ≤ a then a = b (antisymmetry);
-	* If a ≤ b and b ≤ c then a ≤ c (transitivity); (done)
-	* a ≤ b or b ≤ a (totality).
-	* (probably reflexivity too, although that is a consequence of totality) (leid)
-
-	~~Probably can base some of these on [http://code.google.com/p/ghilbert/source/browse/trunk/peano/peano_thms.gh peano_thms.gh]~~

	=== nomenclature: combining vs combination ===		=== nomenclature: combining vs combination ===
	Shouldn't ThereExistsConjunctionCombining be called ThereExistsConjunctionCombination and likewise for any other *Combining theorems?		Shouldn't ThereExistsConjunctionCombining be called ThereExistsConjunctionCombination and likewise for any other *Combining theorems?
-
-	~~=== Basic arithmetic ===~~
-	[[Interface:Basic arithmetic]] did not until recently have anything which needs to be proved with the ZeroNotSuccessor axiom. The issue is which theorems we can use to prove ZeroNotSuccessor in that page where we do such things.
-
-	* The total order properties might rule out modular arithmetic (?), when combined with "5. Inequality is preserved by addition: x ≤ y → x + z ≤ y + z"
-
-	* x ≤ y → x · z ≤ y · z (or ZeroSmallest, or I think some of the others) would rule out integer arithmetic.
-
-	* 1 ≠ 0 needs ZeroNotSuccessor (without it the universe with one object can model the system).

	== More axiomizations of propositional logic ==		== More axiomizations of propositional logic ==

Basic arithmetic implies Peano axioms

Kingdon — Sat, 04 Sep 2010 19:29:08 GMT

add Successor, addition and multiplication, induction, ZeroNotSuccessor

← Older revision		Revision as of 19:29, 4 September 2010
Line 4:		Line 4:
	}}		}}

-	~~{{under construction}}~~
	The idea behind [[Interface:Basic arithmetic]] is that it should include everything we need to conveniently do arithmetic. This module provides a minimal baseline: basic arithmetic should at least be sufficient to prove the Peano axioms. This is not trivially true because basic arithmetic lacks a successor operation and contains few of the axioms in their original form.		The idea behind [[Interface:Basic arithmetic]] is that it should include everything we need to conveniently do arithmetic. This module provides a minimal baseline: basic arithmetic should at least be sufficient to prove the Peano axioms. This is not trivially true because basic arithmetic lacks a successor operation and contains few of the axioms in their original form.

Line 23:		Line 22:
	<jh>		<jh>
	def ((succ a) (a + (1)))		def ((succ a) (a + (1)))
		+	</jh>
		+
		+	Then <code>Successor</code> is a consequence of the addition builder.
		+	<jh>
		+	thm (Successor () () (((succ a) = (succ b)) ↔ (a = b)) (
		+	a (1) b AdditionCancellationRight
		+	))
		+	</jh>
		+
		+	== Addition and multiplication ==
		+
		+	The defining properties of addition and multiplication exist as theorems, or easy consequences of theorems.
		+
		+	<jh>
		+	thm (AdditiveIdentity () () ((a + (0)) = a) (
		+	a AdditiveIdentityRight
		+	))
		+
		+	thm (Addition () () ((a + (succ b)) = (succ (a + b))) (
		+	a b (1) AdditionAssociativity
		+	swapEquality
		+	))
		+
		+	thm (MultiplicativeZero () () ((a · (0)) = (0)) (
		+	a MultiplicativeZeroRight
		+	))
		+
		+	thm (Multiplication () () ((a · (succ b)) = (a + (a · b))) (
		+	b (1) AdditionCommutativity
		+	a buildMultiplicationLL
		+
		+	a (1) b LeftDistribution
		+	applyEqualityTransitivity
		+
		+	a MultiplicativeIdentityRight
		+	(a · b) buildAdditionRR
		+	applyEqualityTransitivity
		+	))
		+	</jh>
		+
		+	== Induction ==
		+
		+	The only thing we need to do with induction is deal with successor versus adding one.
		+	<jh>
		+	thm (Induction () ()
		+	(((subst (0) n φ) ∧
		+	(∀ k ((subst (value k) n φ) → (subst (succ (value k)) n φ))))
		+	→ (∀ n φ)) (
		+	n φ k InductionSubst
		+	))
		+	</jh>
		+
		+	== Zero is not the successor of any number ==
		+	We have saved <code>ZeroNotSuccessor</code> for last, as it is the most difficult and deepest (in terms of distinguishing natural numbers from other structures).
		+
		+	In particular, this proof relies both on <code>0 ≤ a</code>, which rules out negative numbers, and <code>0 ≠ 1</code>, which is needed to establish that more than one number exists.
		+	<jh>
		+	thm (ZeroNotSuccessor () () (¬ ((0) = (succ a))) (
		+	</jh>
		+	We start with <code>0 ≤ a</code> and <code>0 < 1</code>.
		+	<jh>
		+	a ZeroSmallest
		+
		+	(1) ZeroSmallest
		+	ZeroOne
		+	introduceConjunction
		+
		+	(0) (1) LessThanLessEqual
		+	eliminateBiconditionalForward
		+	applyModusPonens
		+	</jh>
		+	Combining these produces <code>0 + 0 < a + 1</code>.
		+	<jh>
		+	introduceConjunction
		+	(0) a (0) (1) LessEqualLessThanAddition
		+	applyModusPonens
		+	</jh>
		+	Simplifyng the left hand side gives <code>0 < a + 1</code>.
		+	<jh>
		+	(0) AdditiveIdentityLeft
		+	(a + (1)) buildLessThanRR
		+	eliminateBiconditionalReverse
		+	applyModusPonens
		+	</jh>
		+	And strict inequality and equality cannot both hold.
		+	<jh>
		+	(0) (a + (1)) LessThanEquality
		+	applyModusPonens
		+	))
	</jh>		</jh>

	== Export ==		== Export ==

-	We're now ready to export [[Interface:Peano axioms]]~~. Or rather, we will be, when this file is done~~.	+	We're now ready to export [[Interface:Peano axioms]].

	<jh>		<jh>
-	#export (PEANO Interface:Peano_axioms (CLASSICAL FIRSTORDER) ())	+	export (PEANO Interface:Peano_axioms (CLASSICAL FIRSTORDER) ())
	</jh>		</jh>

Interface:Basic arithmetic

Kingdon — Sat, 04 Sep 2010 19:26:25 GMT

at most one of a < b, a = b, or a > b hold

← Older revision		Revision as of 19:26, 4 September 2010
Line 159:		Line 159:
	stmt (LessEqualLessThanTransitivity () () (((a ≤ b) ∧ (b < c)) → (a < c)))		stmt (LessEqualLessThanTransitivity () () (((a ≤ b) ∧ (b < c)) → (a < c)))
	stmt (LessThanTransitivity () () (((a < b) ∧ (b < c)) → (a < c)))		stmt (LessThanTransitivity () () (((a < b) ∧ (b < c)) → (a < c)))
		+	</jh>

		+	Exactly one of <code>a < b</code>, <code>a = b</code>, or <code>a > b</code> hold.
		+	<jh>
	stmt (LessThanTotality () () (((a < b) ∨ (a = b)) ∨ (a > b)))		stmt (LessThanTotality () () (((a < b) ∨ (a = b)) ∨ (a > b)))
		+	stmt (LessThanEquality () () ((a < b) → (a ≠ b)))
		+	stmt (LessThanGreaterThan () () ((a < b) → (¬ (a > b))))
		+	stmt (EqualityLessThan () () ((a = b) → (¬ (a < b))))
	</jh>		</jh>

Basic arithmetic

Kingdon — Sat, 04 Sep 2010 19:26:03 GMT

at most one of a < b, a = b, or a > b hold

← Older revision		Revision as of 19:26, 4 September 2010
Line 2,057:		Line 2,057:

	==== Strict order totality ====		==== Strict order totality ====
-	Exactly one of <code~~><nowiki~~>a < b~~</nowiki>~~</code>, <code>a = b</code>, or <code~~><nowiki~~>a > b~~</nowiki>~~</code> holds. We start with the proposition that at least one of the three holds.	+	Exactly one of <code>a < b</code>, <code>a = b</code>, or <code>a > b</code> holds. We start with the proposition that at least one of the three holds.
	<jh>		<jh>
	thm (LessThanTotality () () (((a < b) ∨ (a = b)) ∨ (a > b)) (		thm (LessThanTotality () () (((a < b) ∨ (a = b)) ∨ (a > b)) (
Line 2,086:		Line 2,086:

	swap23ofDisjunction3		swap23ofDisjunction3
		+	))
		+	</jh>
		+
		+	The following theorems imply that no more than one of <code>a < b</code>, <code>a = b</code>, or <code>a > b</code> holds.
		+	<jh>
		+	thm (LessThanEquality () () ((a < b) → (a ≠ b)) (
		+	a b LessThanLessEqual
		+	eliminateBiconditionalReverse
		+
		+	(a ≤ b) (a ≠ b) ConjunctionLeftElimination
		+
		+	applySyllogism
		+	))
		+
		+	thm (LessThanGreaterThan () () ((a < b) → (¬ (a > b))) (
		+	a EqualityReflexivity
		+
		+	</jh>
		+	We start with <code>a < b ∧ b < a → a < a</code>.
		+	<jh>
		+	a b a LessThanTransitivity
		+	</jh>
		+	Using the previous theorem we turn this into <code>a < b ∧ b < a → a ≠ a</code>.
		+	<jh>
		+	a a LessThanEquality
		+	applySyllogism
		+
		+	</jh>
		+	Since <code>a = a</code> is a theorem, this gives us <code>¬ (a < b ∧ b < a)</code>
		+	<jh>
		+	transposeWithNegatedConsequent
		+	applyModusPonens
		+	</jh>
		+	A bit of propositional logic turns this into what we need.
		+	<jh>
		+	distributeNegationPCP
		+	convertToImplicationFromDisjunction
		+	))
		+
		+	thm (EqualityLessThan () () ((a = b) → (¬ (a < b))) (
		+	a b LessThanEquality
		+	transposeWithNegatedConsequent
	))		))
	</jh>		</jh>

Interface:Basic arithmetic

Kingdon — Sat, 04 Sep 2010 18:49:41 GMT

add rule forms of less than builders

← Older revision		Revision as of 18:49, 4 September 2010
Line 161:		Line 161:

	stmt (LessThanTotality () () (((a < b) ∨ (a = b)) ∨ (a > b)))		stmt (LessThanTotality () () (((a < b) ∨ (a = b)) ∨ (a > b)))
		+	</jh>
		+
		+	We also provide some rules, for convenience.
		+	<jh>
		+	stmt (buildLessThan () ((a0 = a1) (b0 = b1)) ((a0 < b0) ↔ (a1 < b1)))
		+	stmt (buildLessThanLL () ((b0 = b1)) ((a < b0) ↔ (a < b1)))
		+	stmt (buildLessThanRR () ((a0 = a1)) ((a0 < b) ↔ (a1 < b)))
	</jh>		</jh>

Basic arithmetic

Kingdon — Sat, 04 Sep 2010 18:49:06 GMT

add rules for less than builders

← Older revision		Revision as of 18:49, 4 September 2010
Line 1,943:		Line 1,943:
	a0 a1 b b LessThanBuilder		a0 a1 b b LessThanBuilder
	detach2of2		detach2of2
		+	))
		+
		+	thm (buildLessThan () ((HA (a0 = a1)) (HB (b0 = b1))) ((a0 < b0) ↔ (a1 < b1)) (
		+	HA
		+	HB
		+	introduceConjunction
		+	a0 a1 b0 b1 LessThanBuilder
		+	applyModusPonens
		+	))
		+
		+	thm (buildLessThanLL () ((HB (b0 = b1))) ((a < b0) ↔ (a < b1)) (
		+	HB
		+	b0 b1 a LessThanBuilderLL
		+	applyModusPonens
		+	))
		+
		+	thm (buildLessThanRR () ((HA (a0 = a1))) ((a0 < b) ↔ (a1 < b)) (
		+	HA
		+	a0 a1 b LessThanBuilderRR
		+	applyModusPonens
	))		))
	</jh>		</jh>

Interface:Basic arithmetic

Kingdon — Sat, 04 Sep 2010 18:02:56 GMT

addition is consistent with the order, ZeroSmallest

← Older revision		Revision as of 18:02, 4 September 2010
Line 161:		Line 161:

	stmt (LessThanTotality () () (((a < b) ∨ (a = b)) ∨ (a > b)))		stmt (LessThanTotality () () (((a < b) ∨ (a = b)) ∨ (a > b)))
		+	</jh>
		+
		+	=== Smallest element ===
		+	Zero is the smallest natural number.
		+	<jh>
		+	stmt (ZeroSmallest () () ((0) ≤ a))
		+	</jh>
		+
		+	=== Addition is consistent with the order ===
		+	Assuming one of these implies the others fairly directly, but we supply them all as convenience theorems.
		+	<jh>
		+	stmt (LessEqualAddition () () (((a0 ≤ a1) ∧ (b0 ≤ b1)) → ((a0 + b0) ≤ (a1 + b1))))
		+	stmt (LessEqualAdditionRR () () ((a0 ≤ a1) ↔ ((a0 + b) ≤ (a1 + b))))
		+	stmt (LessEqualAdditionLL () () ((b0 ≤ b1) ↔ ((a + b0) ≤ (a + b1))))
		+
		+	stmt (LessThanAddition () () (((a0 < a1) ∧ (b0 < b1)) → ((a0 + b0) < (a1 + b1))))
		+	stmt (LessThanAdditionRR () () ((a0 < a1) ↔ ((a0 + b) < (a1 + b))))
		+	stmt (LessThanAdditionLL () () ((b0 < b1) ↔ ((a + b0) < (a + b1))))
		+
		+	stmt (LessEqualLessThanAddition () () (((a0 ≤ a1) ∧ (b0 < b1)) → ((a0 + b0) < (a1 + b1))))
	</jh>		</jh>

Basic arithmetic

Kingdon — Sat, 04 Sep 2010 17:43:26 GMT

add LessThanAdditionRR, LessThanAdditionLL, LessEqualLessThanAddition, LessThanAddition

← Older revision		Revision as of 17:43, 4 September 2010
Line 2,022:		Line 2,022:
	Transitivity for <code><</code> is an immediate consequence.		Transitivity for <code><</code> is an immediate consequence.
	<jh>		<jh>
		+	thm (LessThanLessEqualImplication () () ((a < b) → (a ≤ b)) (
		+	(a ≤ b) (a ≠ b) ConjunctionRightElimination
		+	))
		+
	thm (LessThanTransitivity () () (((a < b) ∧ (b < c)) → (a < c)) (		thm (LessThanTransitivity () () (((a < b) ∧ (b < c)) → (a < c)) (
-	~~</jh>~~	+	a b LessThanLessEqualImplication
-	~~We start with <code>a < b → a ≤ b</code>.~~	+
-	~~<jh>~~	+
-	(a ≤ b~~) (a ≠ b) ConjunctionRightElimination~~	+
-	~~</jh>~~	+
-	~~Adding that to a builders and <code>LessEqualLessThanTransitivity</code> finishes the proof.~~	+
-	~~<jh>~~	+
	(b < c) conjoinRR		(b < c) conjoinRR

Line 2,131:		Line 2,130:
	composeConjunction		composeConjunction
	(a0 + b0) (a1 + b0) (a1 + b1) LessEqualTransitivity		(a0 + b0) (a1 + b0) (a1 + b1) LessEqualTransitivity
		+	applySyllogism
		+	))
		+	</jh>
		+
		+	Here we prove the analogous theorems for the strict order.
		+	<jh>
		+	thm (LessThanAdditionRR () () ((a0 < a1) ↔ ((a0 + b) < (a1 + b))) (
		+	a0 a1 b LessEqualAdditionRR
		+
		+	a0 b a1 AdditionCancellationRight
		+	swapBiconditional
		+	addNegation
		+
		+	buildConjunction
		+	))
		+
		+	thm (LessThanAdditionLL () () ((b0 < b1) ↔ ((a + b0) < (a + b1))) (
		+	b0 b1 a LessEqualAdditionLL
		+
		+	a b0 b1 AdditionCancellationLeft
		+	swapBiconditional
		+	addNegation
		+
		+	buildConjunction
		+	))
		+
		+	thm (LessEqualLessThanAddition () () (((a0 ≤ a1) ∧ (b0 < b1)) → ((a0 + b0) < (a1 + b1))) (
		+	</jh>
		+	First we show <code>a0 ≤ a1 ∧ b0 < b1 → a0 + b0 ≤ a1 + b0</code>.
		+	<jh>
		+	(a0 ≤ a1) (b0 < b1) ConjunctionRightElimination
		+	a0 a1 b0 LessEqualAdditionRR
		+	eliminateBiconditionalReverse
		+	applySyllogism
		+	</jh>
		+	Next is <code>a0 ≤ a1 ∧ b0 < b1 → a1 + b0 < a1 + b1</code>.
		+	<jh>
		+	(a0 ≤ a1) (b0 < b1) ConjunctionLeftElimination
		+	b0 b1 a1 LessThanAdditionLL
		+	eliminateBiconditionalReverse
		+	applySyllogism
		+	</jh>
		+	Combining the two finishes the proof.
		+	<jh>
		+	composeConjunction
		+	(a0 + b0) (a1 + b0) (a1 + b1) LessEqualLessThanTransitivity
		+	applySyllogism
		+	))
		+
		+	thm (LessThanAddition () () (((a0 < a1) ∧ (b0 < b1)) → ((a0 + b0) < (a1 + b1))) (
		+	a0 a1 LessThanLessEqualImplication
		+	(b0 < b1) conjoinRR
		+
		+	a0 a1 b0 b1 LessEqualLessThanAddition
		+
	applySyllogism		applySyllogism
	))		))

Interface:Basic arithmetic

Kingdon — Sat, 04 Sep 2010 15:51:05 GMT

add cancellation, uncomment theorems

← Older revision		Revision as of 15:51, 4 September 2010
Line 49:		Line 49:
	stmt (buildMultiplicationLL () ((b0 = b1)) ((a · b0) = (a · b1)))		stmt (buildMultiplicationLL () ((b0 = b1)) ((a · b0) = (a · b1)))
	stmt (buildMultiplicationRR () ((a0 = a1)) ((a0 · b) = (a1 · b)))		stmt (buildMultiplicationRR () ((a0 = a1)) ((a0 · b) = (a1 · b)))
		+	</jh>
		+
		+	The converse of some of the builders hold and are known as cancellation laws.
		+	<jh>
		+	stmt (AdditionCancellationRight () () (((a + c) = (b + c)) ↔ (a = b)))
		+	stmt (cancelAdditionRight () (((a + c) = (b + c))) (a = b))
		+	stmt (AdditionCancellationLeft () () (((c + a) = (c + b)) ↔ (a = b)))
		+	stmt (cancelAdditionLeft () (((c + a) = (c + b))) (a = b))
	</jh>		</jh>

Line 114:		Line 122:
	As with a [[w:Field (mathematics)\|field]], the additive identity does not equal the multiplicative identity.		As with a [[w:Field (mathematics)\|field]], the additive identity does not equal the multiplicative identity.
	<jh>		<jh>
-	#stmt (ZeroOne () () ((0) ≠ (1)))	+	stmt (ZeroOne () () ((0) ≠ (1)))
	</jh>		</jh>

Line 143:		Line 151:

	stmt (LessEqualLessThan () () ((a ≤ b) ↔ ((a < b) ∨ (a = b))))		stmt (LessEqualLessThan () () ((a ≤ b) ↔ ((a < b) ∨ (a = b))))
-	#stmt (LessThanLessEqual () () ((a < b) ↔ ((a ≤ b) ∧ (a ≠ b))))	+	stmt (LessThanLessEqual () () ((a < b) ↔ ((a ≤ b) ∧ (a ≠ b))))

	stmt (LessThanBuilder () () (((a0 = a1) ∧ (b0 = b1)) → ((a0 < b0) ↔ (a1 < b1))))		stmt (LessThanBuilder () () (((a0 = a1) ∧ (b0 = b1)) → ((a0 < b0) ↔ (a1 < b1))))
	stmt (LessThanBuilderLL () () ((b0 = b1) → ((a < b0) ↔ (a < b1))))		stmt (LessThanBuilderLL () () ((b0 = b1) → ((a < b0) ↔ (a < b1))))
-	# LessThanBuilderRR	+	stmt (LessThanBuilderRR () () ((a0 = a1) → ((a0 < b) ↔ (a1 < b))))
		+
		+	stmt (LessEqualLessThanTransitivity () () (((a ≤ b) ∧ (b < c)) → (a < c)))
		+	stmt (LessThanTransitivity () () (((a < b) ∧ (b < c)) → (a < c)))

-	~~# LessEqualLessThanTransitivity~~
-	~~# LessThanTransitivity~~
	stmt (LessThanTotality () () (((a < b) ∨ (a = b)) ∨ (a > b)))		stmt (LessThanTotality () () (((a < b) ∨ (a = b)) ∨ (a > b)))
	</jh>		</jh>

Basic arithmetic

Kingdon — Sat, 04 Sep 2010 14:36:22 GMT

add LessThanBuilderRR

← Older revision		Revision as of 14:36, 4 September 2010
(3 intermediate revisions not shown)
Line 1,068:		Line 1,068:
	a MultiplicativeIdentityRight		a MultiplicativeIdentityRight
	applyEqualityTransitivity		applyEqualityTransitivity
		+	))
		+	</jh>
		+
		+	One does not equal zero.
		+	<jh>
		+	thm (ZeroOne () () ((0) ≠ (1)) (
		+	(0) ZeroNotSuccessor
	))		))
	</jh>		</jh>
Line 1,904:		Line 1,911:
	That gives us <code>a ≤ b ↔ (a ≤ b ∧ a ≠ b) ∨ a = b</code>. But <code>a ≤ b ∧ a ≠ b</code> is just the definition of <code><</code>, so this is enough.		That gives us <code>a ≤ b ↔ (a ≤ b ∧ a ≠ b) ∨ a = b</code>. But <code>a ≤ b ∧ a ≠ b</code> is just the definition of <code><</code>, so this is enough.
	<jh>		<jh>
		+	))
		+	</jh>
		+
		+	For parallelism, we also provide the definition of <code><</code> as a theorem.
		+	<jh>
		+	thm (LessThanLessEqual () () ((a < b) ↔ ((a ≤ b) ∧ (a ≠ b))) (
		+	(a < b) BiconditionalReflexivity
	))		))
	</jh>		</jh>
Line 1,923:		Line 1,937:
	a a b0 b1 LessThanBuilder		a a b0 b1 LessThanBuilder
	detach1of2		detach1of2
		+	))
		+
		+	thm (LessThanBuilderRR () () ((a0 = a1) → ((a0 < b) ↔ (a1 < b))) (
		+	b EqualityReflexivity
		+	a0 a1 b b LessThanBuilder
		+	detach2of2
	))		))
	</jh>		</jh>
Line 1,991:		Line 2,011:
	</jh>		</jh>

-	~~{{under construction}}~~	+	Combining the two lemmas gives us transitivity for <code>a ≤ b ∧ b < c</code>.
		+	<jh>
		+	thm (LessEqualLessThanTransitivity () () (((a ≤ b) ∧ (b < c)) → (a < c)) (
		+	a b c LessEqualLessThanTransitivity-1
		+	a b c LessEqualLessThanTransitivity-2
		+	composeConjunction
		+	))
		+	</jh>
		+
		+	Transitivity for <code><</code> is an immediate consequence.
		+	<jh>
		+	thm (LessThanTransitivity () () (((a < b) ∧ (b < c)) → (a < c)) (
		+	</jh>
		+	We start with <code>a < b → a ≤ b</code>.
		+	<jh>
		+	(a ≤ b) (a ≠ b) ConjunctionRightElimination
		+	</jh>
		+	Adding that to a builders and <code>LessEqualLessThanTransitivity</code> finishes the proof.
		+	<jh>
		+	(b < c) conjoinRR
		+
		+	a b c LessEqualLessThanTransitivity
		+	applySyllogism
		+	))
		+	</jh>

	==== Strict order totality ====		==== Strict order totality ====

Interface:Basic arithmetic

Kingdon — Fri, 03 Sep 2010 12:36:51 GMT

add more theorems; ones not proved yet are commented out

← Older revision		Revision as of 12:36, 3 September 2010
Line 110:		Line 110:
	stmt (MultiplicativeIdentityLeft () ()		stmt (MultiplicativeIdentityLeft () ()
	(((1) · a) = a))		(((1) · a) = a))
		+	</jh>
		+
		+	As with a [[w:Field (mathematics)\|field]], the additive identity does not equal the multiplicative identity.
		+	<jh>
		+	#stmt (ZeroOne () () ((0) ≠ (1)))
	</jh>		</jh>

Line 127:		Line 132:
	stmt (LessEqualAntisymmetry () () (((a ≤ b) ∧ (b ≤ a)) → (a = b)))		stmt (LessEqualAntisymmetry () () (((a ≤ b) ∧ (b ≤ a)) → (a = b)))
	stmt (LessEqualTotality () () ((a ≤ b) ∨ (b ≤ a)))		stmt (LessEqualTotality () () ((a ≤ b) ∨ (b ≤ a)))
		+	</jh>
		+
		+	A number of other properties follow from those.
		+	<jh>
		+	stmt (LessEqualReflexivity () () (a ≤ a))
		+
		+	term (formula (< nat nat))
		+	def ((> b a) (a < b))
		+	def ((≥ b a) (a ≤ b))
		+
		+	stmt (LessEqualLessThan () () ((a ≤ b) ↔ ((a < b) ∨ (a = b))))
		+	#stmt (LessThanLessEqual () () ((a < b) ↔ ((a ≤ b) ∧ (a ≠ b))))
		+
		+	stmt (LessThanBuilder () () (((a0 = a1) ∧ (b0 = b1)) → ((a0 < b0) ↔ (a1 < b1))))
		+	stmt (LessThanBuilderLL () () ((b0 = b1) → ((a < b0) ↔ (a < b1))))
		+	# LessThanBuilderRR
		+
		+	# LessEqualLessThanTransitivity
		+	# LessThanTransitivity
		+	stmt (LessThanTotality () () (((a < b) ∨ (a = b)) ∨ (a > b)))
	</jh>		</jh>

MediaWiki:Randompage

GrafZahl — Thu, 02 Sep 2010 11:38:09 GMT

random page → random proof module

MediaWiki:Edittools

GrafZahl — Thu, 02 Sep 2010 08:53:22 GMT

+congruence symbol

Wikiproofs:Tearoom

GrafZahl — Thu, 02 Sep 2010 08:08:34 GMT

Reverted edits by 122.159.46.157 (Talk) to last revision by GrafZahl

← Older revision		Revision as of 08:08, 2 September 2010
Line 303:		Line 303:

	:Hi, welcome to the site. Was there any kind of contribution you were particularly interested in? There's plenty to do, from writing proofs to software development to writing explanatory text. [[User:Kingdon\|Kingdon]] 00:13, 19 August 2010 (UTC)		:Hi, welcome to the site. Was there any kind of contribution you were particularly interested in? There's plenty to do, from writing proofs to software development to writing explanatory text. [[User:Kingdon\|Kingdon]] 00:13, 19 August 2010 (UTC)
-
-	~~== Privates Girls ==~~
-
-	~~ich bin immer geil~~

Wikiproofs:Tearoom

122.159.46.157 — Thu, 02 Sep 2010 04:49:35 GMT

Privates Girls: new section

← Older revision		Revision as of 04:49, 2 September 2010
Line 303:		Line 303:

	:Hi, welcome to the site. Was there any kind of contribution you were particularly interested in? There's plenty to do, from writing proofs to software development to writing explanatory text. [[User:Kingdon\|Kingdon]] 00:13, 19 August 2010 (UTC)		:Hi, welcome to the site. Was there any kind of contribution you were particularly interested in? There's plenty to do, from writing proofs to software development to writing explanatory text. [[User:Kingdon\|Kingdon]] 00:13, 19 August 2010 (UTC)
		+
		+	== Privates Girls ==
		+
		+	ich bin immer geil

Basic arithmetic

Kingdon — Thu, 02 Sep 2010 03:45:20 GMT

most of the way to LessEqualLessThanTransitivity

← Older revision		Revision as of 03:45, 2 September 2010
Line 1,917:		Line 1,917:

	buildConjunctionInConsequent		buildConjunctionInConsequent
		+	))
		+
		+	thm (LessThanBuilderLL () () ((b0 = b1) → ((a < b0) ↔ (a < b1))) (
		+	a EqualityReflexivity
		+	a a b0 b1 LessThanBuilder
		+	detach1of2
	))		))
	</jh>		</jh>
		+
		+	==== Transitivity ====
		+	We start by proving that <code>a ≤ b ∧ b < c → a < c</code>. This has transitivity for <code><</code> as an immediate consequence, but will occasionally be useful in its own right.
		+
		+	The first lemma constitutes the easy part of the proof.
		+	<jh>
		+	thm (LessEqualLessThanTransitivity-1 () () (((a ≤ b) ∧ (b < c)) → (a ≤ c)) (
		+	(b ≤ c) (b ≠ c) ConjunctionRightElimination
		+	(a ≤ b) conjoinLL
		+
		+	a b c LessEqualTransitivity
		+	applySyllogism
		+	))
		+	</jh>
		+
		+	The harder part of the proof is that <code>a ≤ b ∧ b < c → a ≠ c</code>. This is fairly easy to sketch out: suppose that <code>a ≤ b ∧ b < c</code> and that <code>a = c</code>. Applying <code>a = c</code> to the first formula gives <code>a ≤ b ∧ b ≤ a</code>, and thus <code>a = b</code> by antisymmetry. But <code>a = b</code> and <code>a = c</code> imply <code>b = c</code>, and this contradicts <code>b < c</code>. Here is one way to formalize that argument.
		+	<jh>
		+	thm (LessEqualLessThanTransitivity-2 () () (((a ≤ b) ∧ (b < c)) → (a ≠ c)) (
		+	</jh>
		+	We start with a substitution, <code>a = c → (a ≤ b ∧ b < a ↔ a ≤ b ∧ b < c)</code>
		+	<jh>
		+	a c b LessThanBuilderLL
		+	(a ≤ b) buildConjunctionLLInConsequent
		+	</jh>
		+	Taking the reverse direction of the biconditional, expanding the definition of <code>b < a</code> and assocating the conjunctions gives <code>a = c → (a ≤ b ∧ b < c → (a ≤ b ∧ b ≤ a) ∧ b ≠ a)</code>
		+	<jh>
		+	eliminateBiconditionalForwardInConsequent
		+
		+	(a ≤ b) (b ≤ a) (b ≠ a) ConjunctionAssociativity
		+	swapBiconditional
		+	transformImplicationImplicationConsequent
		+	</jh>
		+	But <code>a ≤ b ∧ b ≤ a</code> implies <code>b = a</code>,
		+	<jh>
		+	a b LessEqualAntisymmetry
		+
		+	a b EqualitySymmetry
		+	eliminateBiconditionalReverse
		+	applySyllogism
		+	</jh>
		+	so <code>(a ≤ b ∧ b ≤ a) ∧ b ≠ a</code> implies <code>⊥</code> (false).
		+	<jh>
		+	(b ≠ a) conjoinRR
		+
		+	(b = a) Contradiction
		+	eliminateBiconditionalReverse
		+	applySyllogism
		+	</jh>
		+	The next step is <code>(a ≤ b ∧ b < c → (a ≤ b ∧ b ≤ a) ∧ b ≠ a) → ¬ (a ≤ b ∧ b < c)</code>.
		+	<jh>
		+	((a ≤ b) ∧ (b < c)) addCommonAntecedent
		+
		+	((a ≤ b) ∧ (b < c)) NegationImplication
		+	eliminateBiconditionalForward
		+	applySyllogism
		+	</jh>
		+	Combining that with the previous result gives <code>a = c → ¬ (a ≤ b ∧ b < c)</code>.
		+	<jh>
		+	applySyllogism
		+	</jh>
		+	And a transposition finishes the job.
		+	<jh>
		+	transposeWithNegatedConsequent
		+	))
		+	</jh>
		+
		+	{{under construction}}

	==== Strict order totality ====		==== Strict order totality ====

Interface:Classical propositional calculus

Kingdon — Thu, 02 Sep 2010 03:36:38 GMT

add buildConjunctionLLInConsequent

← Older revision		Revision as of 03:36, 2 September 2010
Line 442:		Line 442:
	((antecedent → (p ↔ q)))		((antecedent → (p ↔ q)))
	(antecedent → ((p ∧ common) ↔ (q ∧ common))))		(antecedent → ((p ∧ common) ↔ (q ∧ common))))
		+	stmt (buildConjunctionLLInConsequent ()
		+	((antecedent → (p ↔ q)))
		+	(antecedent → ((common ∧ p) ↔ (common ∧ q))))
	stmt (buildDisjunctionRRInConsequent () ((antecedent → (p ↔ q))) (antecedent → ((p ∨ common) ↔ (q ∨ common))))		stmt (buildDisjunctionRRInConsequent () ((antecedent → (p ↔ q))) (antecedent → ((p ∨ common) ↔ (q ∨ common))))
	stmt (buildDisjunctionLLInConsequent () ((antecedent → (p ↔ q))) (antecedent → ((common ∨ p) ↔ (common ∨ q))))		stmt (buildDisjunctionLLInConsequent () ((antecedent → (p ↔ q))) (antecedent → ((common ∨ p) ↔ (common ∨ q))))

Convenience theorems of propositional logic

Kingdon — Thu, 02 Sep 2010 03:35:16 GMT

add buildConjunctionLLInConsequent

← Older revision		Revision as of 03:35, 2 September 2010
Line 361:		Line 361:
	common BiconditionalReflexivity		common BiconditionalReflexivity
	p q common common ConjunctionFunction detach2of2		p q common common ConjunctionFunction detach2of2
		+	applySyllogism
		+	))
		+
		+	thm (buildConjunctionLLInConsequent ()
		+	((H (antecedent → (p ↔ q))))
		+	(antecedent → ((common ∧ p) ↔ (common ∧ q))) (
		+	H
		+	common BiconditionalReflexivity
		+	common common p q ConjunctionFunction detach1of2
	applySyllogism		applySyllogism
	))		))

Basic arithmetic

Kingdon — Wed, 01 Sep 2010 18:52:12 GMT

add LessEqualAdditionLL, LessEqualAddition

← Older revision		Revision as of 18:52, 1 September 2010
Line 1,979:		Line 1,979:
	swapBiconditional		swapBiconditional
	applyBiconditionalTransitivity		applyBiconditionalTransitivity
		+	))
		+	</jh>
		+
		+	Here is the same theorem with the additions commuted.
		+	<jh>
		+	thm (LessEqualAdditionLL () () ((b0 ≤ b1) ↔ ((a + b0) ≤ (a + b1))) (
		+	b0 b1 a LessEqualAdditionRR
		+
		+	b0 a AdditionCommutativity
		+	b1 a AdditionCommutativity
		+	buildLessEqual
		+
		+	applyBiconditionalTransitivity
		+	))
		+	</jh>
		+
		+	Combining the two gives the full theorem.
		+	<jh>
		+	thm (LessEqualAddition () () (((a0 ≤ a1) ∧ (b0 ≤ b1)) → ((a0 + b0) ≤ (a1 + b1))) (
		+	(a0 ≤ a1) (b0 ≤ b1) ConjunctionRightElimination
		+	a0 a1 b0 LessEqualAdditionRR
		+	eliminateBiconditionalReverse
		+	applySyllogism
		+	</jh>
		+	That gives us <code>a0 ≤ a1 ∧ b0 ≤ b1 → a0 + b0 ≤ a1 + b0</code>. Now we apply a similar technique to also get <code>a0 ≤ a1 ∧ b0 ≤ b1 → a1 + b0 ≤ a1 + b1</code>.
		+	<jh>
		+	(a0 ≤ a1) (b0 ≤ b1) ConjunctionLeftElimination
		+	b0 b1 a1 LessEqualAdditionLL
		+	eliminateBiconditionalReverse
		+	applySyllogism
		+	</jh>
		+	Combining these two finishes the proof.
		+	<jh>
		+	composeConjunction
		+	(a0 + b0) (a1 + b0) (a1 + b1) LessEqualTransitivity
		+	applySyllogism
	))		))
	</jh>		</jh>

User talk:Kingdon

Kingdon — Wed, 01 Sep 2010 17:52:20 GMT

wikiproofs.org: proofwiki.org

← Older revision		Revision as of 17:52, 1 September 2010
Line 84:		Line 84:

	Hi, today I registered the domain [http://www.wikiproofs.org wikiproofs.org] in addition to wikiproofs.de. The .org domain seems more appropriate for an international non-profit project. My provider tells me that it may take up to 48 hours until the new domain correctly resolves to the Wikiproofs host everywhere in the world. I'd have registered the .org domain earlier but there used to be another site sitting on it (possibly intended as a non-formal proof wiki, but it always looked kinda defunct to me). I'll try to switch MediaWiki and the web server over to use .org by default when the 48 hours have passed.--[[User:GrafZahl\|GrafZahl]] ([[User talk:GrafZahl\|talk]]) 16:35, 1 September 2010 (UTC)		Hi, today I registered the domain [http://www.wikiproofs.org wikiproofs.org] in addition to wikiproofs.de. The .org domain seems more appropriate for an international non-profit project. My provider tells me that it may take up to 48 hours until the new domain correctly resolves to the Wikiproofs host everywhere in the world. I'd have registered the .org domain earlier but there used to be another site sitting on it (possibly intended as a non-formal proof wiki, but it always looked kinda defunct to me). I'll try to switch MediaWiki and the web server over to use .org by default when the 48 hours have passed.--[[User:GrafZahl\|GrafZahl]] ([[User talk:GrafZahl\|talk]]) 16:35, 1 September 2010 (UTC)
		+
		+	:Hmm. The .org is probably a bit easier to confuse with [http://www.proofwiki.org/wiki/Main_Page proofwiki.org] which as far as I can tell is non-defunct. But use your best judgement. [[User:Kingdon\|Kingdon]] 17:52, 1 September 2010 (UTC)

User talk:Kingdon

GrafZahl — Wed, 01 Sep 2010 16:35:51 GMT

wikiproofs.org: new section

← Older revision		Revision as of 16:35, 1 September 2010
Line 80:		Line 80:

	:Thanks for keeping me informed. Doesn't sound like there is anything worth doing about it unless perhaps if it starts happening often. [[Special:Contributions/97.73.64.163\|97.73.64.163]] 21:52, 28 August 2010 (UTC)		:Thanks for keeping me informed. Doesn't sound like there is anything worth doing about it unless perhaps if it starts happening often. [[Special:Contributions/97.73.64.163\|97.73.64.163]] 21:52, 28 August 2010 (UTC)
		+
		+	== wikiproofs.org ==
		+
		+	Hi, today I registered the domain [http://www.wikiproofs.org wikiproofs.org] in addition to wikiproofs.de. The .org domain seems more appropriate for an international non-profit project. My provider tells me that it may take up to 48 hours until the new domain correctly resolves to the Wikiproofs host everywhere in the world. I'd have registered the .org domain earlier but there used to be another site sitting on it (possibly intended as a non-formal proof wiki, but it always looked kinda defunct to me). I'll try to switch MediaWiki and the web server over to use .org by default when the 48 hours have passed.--[[User:GrafZahl\|GrafZahl]] ([[User talk:GrafZahl\|talk]]) 16:35, 1 September 2010 (UTC)

User talk:GrafZahl

GrafZahl — Wed, 01 Sep 2010 09:49:55 GMT

publicity: thanks

← Older revision		Revision as of 09:49, 1 September 2010
Line 37:		Line 37:

	::In two paragraphs I won't have the space to go into any details on what's missing from wikiproofs, but I'll see if there is a natural way to work in the bit about mixing informal text with the proofs (which I agree is important, including diagrams, see for example the SVG diagram under Pasch's axiom at [[Interface:Tarski's geometry axioms]], without which I certainly can't follow all the u's and v's). I figure the whole thing is pretty tentative until I hear more about their style guidelines, a somewhat more solid statement of whether they want to run the piece, etc, but I have written back to Prof. Henle to keep the ball rolling. [[User:Kingdon\|Kingdon]] 03:47, 1 September 2010 (UTC)		::In two paragraphs I won't have the space to go into any details on what's missing from wikiproofs, but I'll see if there is a natural way to work in the bit about mixing informal text with the proofs (which I agree is important, including diagrams, see for example the SVG diagram under Pasch's axiom at [[Interface:Tarski's geometry axioms]], without which I certainly can't follow all the u's and v's). I figure the whole thing is pretty tentative until I hear more about their style guidelines, a somewhat more solid statement of whether they want to run the piece, etc, but I have written back to Prof. Henle to keep the ball rolling. [[User:Kingdon\|Kingdon]] 03:47, 1 September 2010 (UTC)
		+
		+	:::OK, thank you very much! Also thanks for updating [[WP:ABOUT]]!--[[User:GrafZahl\|GrafZahl]] 09:49, 1 September 2010 (UTC)

Interface:Tarski's geometry axioms

GrafZahl — Wed, 01 Sep 2010 08:53:04 GMT

fixing defaultsort syntax

← Older revision		Revision as of 08:53, 1 September 2010
(One intermediate revision not shown)
Line 80:		Line 80:
	* [[w:Tarski's axioms]], citing Tarski, Alfred; Givant, Steven (1999), "Tarski's system of geometry", The Bulletin of Symbolic Logic 5 (2): 175–214, doi:10.2307/421089, MR1791303, ISSN 1079-8986		* [[w:Tarski's axioms]], citing Tarski, Alfred; Givant, Steven (1999), "Tarski's system of geometry", The Bulletin of Symbolic Logic 5 (2): 175–214, doi:10.2307/421089, MR1791303, ISSN 1079-8986

-	~~[[Category~~:~~Geometry\|~~{{PAGENAME}}]]	+	{{DEFAULTSORT:{{PAGENAME}}}}
		+	[[Category:Euclidean geometries (general) and generalizations]]
		+	[[Category:Foundations of classical theories (including reverse mathematics)]]

Category:Foundations of classical theories (including reverse mathematics)

GrafZahl — Wed, 01 Sep 2010 08:41:24 GMT

created

New page

{{msc2010|03B30|Foundations of classical theories (including reverse mathematics)}}

[[Category:General logic]]

Category:Euclidean geometries (general) and generalizations

GrafZahl — Wed, 01 Sep 2010 08:38:37 GMT

created

New page

{{msc2010|51M05|Euclidean geometries (general) and generalizations}}

[[Category:Real and complex geometry]]

Category:Real and complex geometry

GrafZahl — Wed, 01 Sep 2010 08:37:21 GMT

created

New page

{{msc2010|51Mxx|Real and complex geometry}}

[[Category:Geometry]]

Category:Geometry

GrafZahl — Wed, 01 Sep 2010 08:21:06 GMT

created

New page

{{msc2010|51-XX|Geometry}}

[[Category:Mathematics Subject Classification]]

Interface:Tarski's geometry axioms

Kingdon — Wed, 01 Sep 2010 03:50:59 GMT

link to wikipedia page

← Older revision		Revision as of 03:50, 1 September 2010
Line 5:		Line 5:
	\| right =		\| right =
	\| shortcut =		\| shortcut =
-	\| notes = Since [[w:Euclid\|Euclid]], compass-and-straightedge geometry has been presented as following from postulates. However, it was not until the 20th century that a complete set of postulates were put forward. This page is for one such set, the first-order axiomization by Tarski. It makes reference to points (not directly to lines, angles, or circles), and has two relationships between points: betweenness and congruence.	+	\| notes = Since [[w:Euclid\|Euclid]], compass-and-straightedge geometry has been presented as following from postulates. However, it was not until the 20th century that a complete set of postulates were put forward. This page is for one such set, the [[w:Tarski's axioms\|first-order axiomization by Tarski]]. It makes reference to points (not directly to lines, angles, or circles), and has two relationships between points: betweenness and congruence.
	}}		}}
	{{modules		{{modules

User talk:GrafZahl

Kingdon — Wed, 01 Sep 2010 03:47:29 GMT

publicity: OK, will work on this

← Older revision		Revision as of 03:47, 1 September 2010
Line 35:		Line 35:

	:--[[User:GrafZahl\|GrafZahl]] 17:30, 31 August 2010 (UTC)		:--[[User:GrafZahl\|GrafZahl]] 17:30, 31 August 2010 (UTC)
		+
		+	::In two paragraphs I won't have the space to go into any details on what's missing from wikiproofs, but I'll see if there is a natural way to work in the bit about mixing informal text with the proofs (which I agree is important, including diagrams, see for example the SVG diagram under Pasch's axiom at [[Interface:Tarski's geometry axioms]], without which I certainly can't follow all the u's and v's). I figure the whole thing is pretty tentative until I hear more about their style guidelines, a somewhat more solid statement of whether they want to run the piece, etc, but I have written back to Prof. Henle to keep the ball rolling. [[User:Kingdon\|Kingdon]] 03:47, 1 September 2010 (UTC)

Wikiproofs:About

Kingdon — Wed, 01 Sep 2010 03:23:04 GMT

add section "Proofs live in wiki pages"

← Older revision		Revision as of 03:23, 1 September 2010
Line 27:		Line 27:

	Without David Hilbert, Norman Megill and Raph Levien, the Wikiproofs project would not have been possible.		Without David Hilbert, Norman Megill and Raph Levien, the Wikiproofs project would not have been possible.
		+
		+	== Proofs live in wiki pages ==
		+	Putting proofs in wiki pages is not just a convenient way of getting proofs up on the web. A wiki is built for collaboration, and getting a sufficient body of collaborators is key to the success of any formalized math project.
		+
		+	Another key goal of the wiki is that we want to be able to intersperse formal proofs with text (formatted using italics, headers, etc), images (for example, diagrams in geometry proofs), formulas (in TeX or unicode text), and anything else that can be done by mediawiki (the wiki which we use, which is also used for wikipedia and many other wikis).

	== Links ==		== Links ==

Interface:Tarski's geometry axioms

Kingdon — Wed, 01 Sep 2010 03:08:46 GMT

add diagram for Pasch's axiom

← Older revision		Revision as of 03:08, 1 September 2010
Line 61:		Line 61:
	</jh>		</jh>

-	[[File:Pasch.svg\|~~right~~\|~~150px\|Axiom of Pasch~~]]	+	=== Pasch's axiom ===
-	[[w:Axiom of Pasch]]	+	[[File:Tarski's formulation of Pasch's axiom.svg\|left\|thumb]]
		+	Tarski's version of the [[w:Axiom of Pasch]].
		+	{{clear}}
	<jh>		<jh>
	stmt (Pasch () () (((between x u z) ∧ (between y v z)) → (∃ a ((between u (value a) y) ∧ (between v (value a) x)))))		stmt (Pasch () () (((between x u z) ∧ (between y v z)) → (∃ a ((between u (value a) y) ∧ (between v (value a) x)))))
	</jh>		</jh>

-	Continuity	+	=== Continuity ===
	<jh>		<jh>
	var (formula φx ψy)		var (formula φx ψy)

Template:Clear

Kingdon — Wed, 01 Sep 2010 02:56:09 GMT

add template; same as in en.wikipedia.org

New page

<div style="clear:both"></div><noinclude>Makes content wait until existing content is completed in all columns. See [[w:Template:Clear]] for further details.</noinclude>

User talk:GrafZahl

GrafZahl — Tue, 31 Aug 2010 17:30:39 GMT

publicity: sure

← Older revision		Revision as of 17:30, 31 August 2010
Line 22:		Line 22:

	Anyway, let me know what you think about the journal. [[User:Kingdon\|Kingdon]] 21:07, 30 August 2010 (UTC)		Anyway, let me know what you think about the journal. [[User:Kingdon\|Kingdon]] 21:07, 30 August 2010 (UTC)
		+
		+	:I read a few articles of the free first 2009 issue of the journal (no Media Highlights were available for free, however) and it looks interesting.
		+	:Indeed, one of my motivations for creating this site was educational in nature: the ability to write down a machine-verifiable theory with the possibility of inserting explanatory wikitext everywhere. This is mentioned briefly on [[mw:Extension:JHilbert#Usage]], but it should get at least a paragraph or so on [[WP:ABOUT]] and possibly the [[Main Page]]. It's one of the things intended to enhance the metamath experience. In metamath, you only get an introductory text and then one whole database item in one chunk. The other important educational factor is, as you mention, the ability to contribute new theories and proofs. I think that both aspects are very important.
		+	:Alas, these features are far from being ready yet. Core issues aside (the currently implemented definition mechanism is ''broken'', no denying it), both JHilbert input and output are in need of certain improvements in order to be of real educational value. The JHilbert renderer is, at this point, merely a glorified syntax highlighter. Metamath is miles ahead of Wikiproofs in this respect. Ideally, the output should display the top of the expression stack after each statement step, and have some JavaScript gizmos to explore the entire proof state on request. As for input, I like Raph's "instant gratification" idea (to be even more instant in proof checking than pressing the preview button, also with JavaScript). In total, the JHilbert integration with MediaWiki is still very, very ad hoc.
		+	:Nevertheless, I don't think we should miss this opportunity and try to publish your short article. However, for the sake of honesty, I think we should highlight at least the following points:
		+	:* currently unfixed core bugs, including an unsound definition mechanism,
		+	:* the current, unfinished, state of JHilbert's tools regarding contribution and presentation makes the site more interesting for educators willing to take up some of the tasks and meta-tasks which must be completed to make Wikiproofs a worthwhile educational experience, rather than for educatees.
		+	:What do you think?
		+
		+	:Finally, I thank you once again, for taking the initiative to increase public awareness of Wikiproofs at a time when I myself have but little time to contribute. Thank you! I also understand that Prof. Henle has taken the time to have a glance at the Wikiproofs site, so I thank him, too.
		+	:As for Quine, let me tell you an anecdote about a revelational moment in my life. I've been casually interested in the foundations of mathematics since my first university semester. It didn't take very long until I found Nicod's article [[s:A Reduction in the number of the Primitive Propositions of Logic\|A Reduction in the number of the Primitive Propositions of Logic]], where he builds the classical propositional calculus from one connective, one axiom and one rule of inference. One day, I worked through the entire paper. It wasn't too easy. I scribbled a veritable stack of papers full, redoing the proofs. But it wasn't too hard, either. It took me the whole day, but not longer. Therefore, I was very surprised that there was sort of a small controversy about the correctness of Nicod's paper. The (partially justified) criticism was that Nicod's proof style was rather terse, and sometimes did not follow the logical order. One Prof. Jörgensen attempted to re-render Nicod's proof in a style similar to what you would feed a modern proof verifier. Alas, he got confused by some of the abbreviations and made improper substitutions in the proof of <code>(t \| (t \| t))</code>. (The error actually made it into a textbook.) I checked my notes and found I had not made such an error. The error was finally cleared up by Quine in 1932, when he wrote a paper with the sole purpose to correctly re-render the proof of <code>(t \| (t \| t))</code> in PM style. So I wondered: why did it take the great Quine to explain Nicod's proof to the general public, twelve years after it was published, when the same proof became clear to me within a single day? The answer is, I believe, ''hindsight''. Before I got Nicod's paper into my hands, I had already read several expository text books and course scripts on formal logic. In fact, it was in a footnote in one of the course scripts where I found the reference to Nicod's article. These beginner's texts had taught me how formal mathematics works, had warned me about common fallacies, before I even knew of the existence of Nicod's axiom. The people in the 1920s, when formal logic was still a very new thing, didn't have these advantages. To grasp a genuinely new idea such as Nicod's must have been much more difficult for people back then than it is for us beginner's-exposition-spoiled folks today. It's also one reason why I believe in the importance of an educationally valuable presentation. It saves time and is less likely to leave you with misconceptions.
		+
		+	:--[[User:GrafZahl\|GrafZahl]] 17:30, 31 August 2010 (UTC)

Help:Tutorial

GrafZahl — Tue, 31 Aug 2010 15:44:24 GMT

typo

← Older revision		Revision as of 15:44, 31 August 2010
Line 1:		Line 1:
-	This is a small '''tutorial''' on how to use the [[mw:~~Extensions~~:JHilbert\|JHilbert]], the automated proof verifier driving this wiki. We shall prove the statement "two plus two equals four" from a small set of simple axioms.	+	This is a small '''tutorial''' on how to use the [[mw:Extension:JHilbert\|JHilbert]], the automated proof verifier driving this wiki. We shall prove the statement "two plus two equals four" from a small set of simple axioms.

	If you're really, ''really'' impatient, you can skip all the preliminary blah blah and jump right to the [[Interface:Tutorial\|implementation of some of the Peano axioms]].		If you're really, ''really'' impatient, you can skip all the preliminary blah blah and jump right to the [[Interface:Tutorial\|implementation of some of the Peano axioms]].

Interface:Tarski's geometry axioms

Kingdon — Tue, 31 Aug 2010 03:12:43 GMT

start in

New page

{{header
| title = Tarski's axioms
| subtitle =
| left =
| right =
| shortcut =
| notes = Since [[w:Euclid|Euclid]], compass-and-straightedge geometry has been presented as following from postulates. However, it was not until the 20th century that a complete set of postulates were put forward. This page is for one such set, the first-order axiomization by Tarski. It makes reference to points (not directly to lines, angles, or circles), and has two relationships between points: betweenness and congruence.
}}
{{modules
| parameters = [[Interface:Classical propositional calculus|Classical propositional calculus]], [[Interface:First-order logic with quantifiability]]
| importedby = None yet
| exportedby = None yet.
}}

First, we adopt the axioms of [[Interface:Classical propositional calculus|propositional logic]] and [[Interface:First-order logic with quantifiability|first-order logic]] (including equality):

<jh>
param (CLASSICAL Interface:Classical_propositional_calculus () ())
param (FIRSTORDER Interface:First-order_logic_with_quantifiability (CLASSICAL) ())
</jh>

The kind <code>object</code>, defined in first-order logic, represents a point:
<jh>
kindbind (object point)
var (point x y z w u v)

var (variable a b c)
</jh>

== Congruence ==
We introduce congruence; <code>(x y ≡ w z)</code> means that the line segment xy is the same length as the line segment wz.
<jh>
term (formula (≡ point point point point))
</jh>

The distance from x to y is the same as the distance from y to x. This property is called reflexivity.
<jh>
stmt (CongruenceReflexivity () () (x y ≡ y x))
</jh>

A segment which has zero length starts and ends at the same point (although saying "zero length" is a bit of a shortcut, as the axioms are not based on real numbers or any other numbers).
<jh>
stmt (CongruenceIdentity () () ((x y ≡ z z) → (x = y)))
</jh>

Two segments which are congruent to a common segment are congruent to each other.
<jh>
stmt (CongruenceTransitivity () () (((x y ≡ z u) ∧ (x y ≡ v w)) → (z u ≡ v w)))
</jh>

== Betweenness ==
The other fundamental formula is betweenness; <code>(between x y z)</code> signifies "y is between x and z".

<jh>
term (formula (between point point point))
</jh>

There are no other points between x and x.
<jh>
stmt (Indivisibility () () ((between x y x) → (x = y)))
</jh>

[[File:Pasch.svg|right|150px|Axiom of Pasch]]
[[w:Axiom of Pasch]]
<jh>
stmt (Pasch () () (((between x u z) ∧ (between y v z)) → (∃ a ((between u (value a) y) ∧ (between v (value a) x)))))
</jh>

Continuity
<jh>
var (formula φx ψy)
#stmt (Continuity ((φx y) (φx a) (φx b) (ψy x) (ψy a) (ψy b)) () ())
</jh>

{{under construction}}

== References ==
* [[w:Tarski's axioms]], citing Tarski, Alfred; Givant, Steven (1999), "Tarski's system of geometry", The Bulletin of Symbolic Logic 5 (2): 175–214, doi:10.2307/421089, MR1791303, ISSN 1079-8986

[[Category:Geometry|{{PAGENAME}}]]

Interface:Peano axioms

Kingdon — Tue, 31 Aug 2010 02:11:42 GMT

fix one more place where we didn't update for the switch to Interface:First-order logic with quantifiability

← Older revision		Revision as of 02:11, 31 August 2010
Line 8:		Line 8:
	}}		}}
	{{modules		{{modules
-	\| parameters = [[Interface:Classical propositional calculus\|Classical propositional calculus]], [[Interface:First-order logic]]	+	\| parameters = [[Interface:Classical propositional calculus\|Classical propositional calculus]], [[Interface:First-order logic with quantifiability]]
	\| importedby = [[Basic arithmetic]]		\| importedby = [[Basic arithmetic]]
	\| exportedby = None yet.		\| exportedby = None yet.

User talk:GrafZahl

Kingdon — Mon, 30 Aug 2010 21:07:09 GMT

publicity: new section

← Older revision		Revision as of 21:07, 30 August 2010
Line 14:		Line 14:

	::::::I'm also out of ideas. Nice to hear that you have a means of making it work for you again. I'm re-enabling the cookie check. According to some MediaWiki mailing list entries, it's a convenience check only, to inform users of cookie loss as soon as possible. Apparently, this check can misfire with certain browser/OS combinations. The debug log is pretty useless because it's lacking timestamps, but I finally found <code>Session user ID (0) and cookie user ID (4) don't match!</code>. (The relevant code is on line 817 in <code>User.php</code>.) I have not investigated why these didn't match in your case. Wikipedia uses a different set of cookies due to SUL. Hence our problem might not apply to Wikipedia. It might also be some PHP session problem at Wikiproof's end.--[[User:GrafZahl\|GrafZahl]] 10:45, 30 August 2010 (UTC)		::::::I'm also out of ideas. Nice to hear that you have a means of making it work for you again. I'm re-enabling the cookie check. According to some MediaWiki mailing list entries, it's a convenience check only, to inform users of cookie loss as soon as possible. Apparently, this check can misfire with certain browser/OS combinations. The debug log is pretty useless because it's lacking timestamps, but I finally found <code>Session user ID (0) and cookie user ID (4) don't match!</code>. (The relevant code is on line 817 in <code>User.php</code>.) I have not investigated why these didn't match in your case. Wikipedia uses a different set of cookies due to SUL. Hence our problem might not apply to Wikipedia. It might also be some PHP session problem at Wikiproof's end.--[[User:GrafZahl\|GrafZahl]] 10:45, 30 August 2010 (UTC)
		+
		+	== publicity ==
		+
		+	I had a nice talk with an old professor of mine, Michael Henle, and he thought that if I wrote a two paragraph summary of wikiproofs for the journal he edits, they'd likely publish it. Sounds like a good idea to me. The pitch would likely be as something to use in education. The only reason I can think of not to do it is if we want wikiproofs to be more "ready" first, but I was thinking of pitching it in terms of ''contributing'' to wikiproofs being the educational thing. I figure the more people hear of wikiproofs, the greater the chance that one of them will have the time to fix definitions, or get set theory moving faster, or prove all those compass-and-straightedge geometry theorems which I kind of doubt I'll have time for. (At least in the US, geometry is perhaps the most obvious hook for educational use of the site, as that is where they teach proofs - although the axiomizations of Hilbert, Tarski, or Birkhoff might be a bit far from the way things are taught in Euclid, or modern textbooks). For more on the journal, see "Media Highlights" at [http://www.maa.org/pubs/cmj_info.html].
		+
		+	Prof. Henle also showed me the historical marker to Quine which is now sitting outside the building where his office is, which was quite a welcome surprise, since I'd vaugely been thinking of looking up the Quine paper which is cited in metamath.
		+
		+	Anyway, let me know what you think about the journal. [[User:Kingdon\|Kingdon]] 21:07, 30 August 2010 (UTC)

Basic arithmetic

Kingdon — Mon, 30 Aug 2010 20:21:32 GMT

add Addition3, LessEqualAdditionRR, biconditionalize AdditionCancellationRight

← Older revision		Revision as of 20:21, 30 August 2010
(One intermediate revision not shown)
Line 471:		Line 471:
	Now we can prove our addition cancellation theorem:		Now we can prove our addition cancellation theorem:
	<jh>		<jh>
-	thm (~~AdditionCancellationRight~~ ((n a) (n b) (n c) (n k) (k a) (k b)) () (((a + c) = (b + c)) → (a = b)) (	+	thm (AdditionCancellationRightForward ((n a) (n b) (n c) (n k) (k a) (k b)) () (((a + c) = (b + c)) → (a = b)) (
	</jh>		</jh>
	We proceed by induction on <code>c</code>.		We proceed by induction on <code>c</code>.
Line 505:		Line 505:

	Induction6S		Induction6S
		+	))
		+	</jh>
		+
		+	As we tend to do with theorems which hold in both directions, we provide the biconditionalized version.
		+	<jh>
		+	thm (AdditionCancellationRight () () (((a + c) = (b + c)) ↔ (a = b)) (
		+	a c b AdditionCancellationRightForward
		+	a b c AdditionBuilderRR
		+	introduceBiconditionalFromImplications
	))		))

Line 510:		Line 519:
	H		H
	a c b AdditionCancellationRight		a c b AdditionCancellationRight
		+	eliminateBiconditionalReverse
	applyModusPonens		applyModusPonens
	))		))
Line 518:		Line 528:
	<jh>		<jh>
	thm (AdditionCancellationLeft () ()		thm (AdditionCancellationLeft () ()
-	(((c + a) = (c + b)) → (a = b)) (	+	(((c + a) = (c + b)) ↔ (a = b)) (
	c a AdditionCommutativity		c a AdditionCommutativity
	c b AdditionCommutativity		c b AdditionCommutativity
	buildEquality		buildEquality
-	~~eliminateBiconditionalReverse~~

	a c b AdditionCancellationRight		a c b AdditionCancellationRight
-	~~applySyllogism~~	+	applyBiconditionalTransitivity
	))		))

Line 533:		Line 542:
	H		H
	c a b AdditionCancellationLeft		c a b AdditionCancellationLeft
		+	eliminateBiconditionalReverse
	applyModusPonens		applyModusPonens
	))		))
Line 795:		Line 805:

	== Rearrangement ==		== Rearrangement ==
-	Although there are a wide varieties of ways that a term could be rearranged by commutativity and associativity, the following ~~rearrangement turns~~ out to be ~~one of the~~ common ~~ones~~:	+	Although there are a wide varieties of ways that a term could be rearranged by commutativity and associativity, the following rearrangements turn out to be common:
	<jh>		<jh>
	thm (Addition4 () () (((a + b) + (c + d)) = ((a + c) + (b + d))) (		thm (Addition4 () () (((a + b) + (c + d)) = ((a + c) + (b + d))) (
Line 814:		Line 824:

	a c (b + d) AdditionAssociativity swapEquality		a c (b + d) AdditionAssociativity swapEquality
		+	applyEqualityTransitivity
		+	))
		+
		+	thm (Addition3 () () (((a + b) + c) = ((a + c) + b)) (
		+	a b c AdditionAssociativity
		+
		+	b c AdditionCommutativity
		+	a buildAdditionLL
		+	applyEqualityTransitivity
		+
		+	a c b AdditionAssociativity
		+	swapEquality
	applyEqualityTransitivity		applyEqualityTransitivity
	))		))
Line 1,301:		Line 1,323:

	((a + ab) + bc) b c AdditionCancellationRight		((a + ab) + bc) b c AdditionCancellationRight
		+	eliminateBiconditionalReverse
	applySyllogism		applySyllogism
	</jh>		</jh>
Line 1,483:		Line 1,506:
	<jh>		<jh>
	a ((value n) + (value m)) (0) AdditionCancellationLeft		a ((value n) + (value m)) (0) AdditionCancellationLeft
		+	eliminateBiconditionalReverse
	applySyllogism		applySyllogism
	</jh>		</jh>
Line 1,828:		Line 1,852:

	==== Strict order ====		==== Strict order ====
-	Here we define <code>~~<nowiki><</nowiki>~~</code>, as well as <code>~~<nowiki>></nowiki>~~</code> and <code>≥</code>.	+	Here we define <code><</code>, as well as <code>></code> and <code>≥</code>.
	<jh>		<jh>
	def ((< a b) ((a ≤ b) ∧ (a ≠ b)))		def ((< a b) ((a ≤ b) ∧ (a ≠ b)))
Line 1,878:		Line 1,902:
	applyBiconditionalTransitivity		applyBiconditionalTransitivity
	</jh>		</jh>
-	That gives us <code>a ≤ b ↔ (a ≤ b ∧ a ≠ b) ∨ a = b</code>. But <code>a ≤ b ∧ a ≠ b</code> is just the definition of <code>~~<nowiki><</nowiki>~~</code>, so this is enough.	+	That gives us <code>a ≤ b ↔ (a ≤ b ∧ a ≠ b) ∨ a = b</code>. But <code>a ≤ b ∧ a ≠ b</code> is just the definition of <code><</code>, so this is enough.
	<jh>		<jh>
		+	))
		+	</jh>
		+
		+	The builder for <code><</code> is a consequence of the one for <code>≤</code>.
		+
		+	<jh>
		+	thm (LessThanBuilder () () (((a0 = a1) ∧ (b0 = b1)) → ((a0 < b0) ↔ (a1 < b1))) (
		+	a0 a1 b0 b1 LessEqualBuilder
		+
		+	a0 a1 b0 b1 EqualityBuilder
		+	addNegationInConsequent
		+
		+	buildConjunctionInConsequent
	))		))
	</jh>		</jh>
Line 1,913:		Line 1,950:

	swap23ofDisjunction3		swap23ofDisjunction3
		+	))
		+	</jh>
		+
		+	=== This order is consistent with addition ===
		+	<jh>
		+	thm (LessEqualAdditionRR ((a n) (b n) (c n)) () ((a ≤ b) ↔ ((a + c) ≤ (b + c))) (
		+	a b n LessEqual
		+	</jh>
		+	The right hand side is now <code>∃ n a + n = b</code>. We add <code>c</code> to both sides of the equality,
		+	<jh>
		+	(a + (value n)) c b AdditionCancellationRight
		+	swapBiconditional
		+	</jh>
		+	rewrite it as <code>(a + c) + n = b + c</code>,
		+	<jh>
		+	a (value n) c Addition3
		+	(b + c) buildEqualityRR
		+	applyBiconditionalTransitivity
		+	</jh>
		+	and reinstate the quantifier to get <code>a ≤ b ↔ ∃ n (a + c) + n = b + c</code>.
		+	<jh>
		+	n buildThereExists
		+	applyBiconditionalTransitivity
		+	</jh>
		+	Applying <code>LessEqual</code> we are done.
		+	<jh>
		+	(a + c) (b + c) n LessEqual
		+	swapBiconditional
		+	applyBiconditionalTransitivity
	))		))
	</jh>		</jh>

Interface:Classical propositional calculus

Kingdon — Mon, 30 Aug 2010 19:02:13 GMT

add buildConjunctionInConsequent

← Older revision		Revision as of 19:02, 30 August 2010
Line 444:		Line 444:
	stmt (buildDisjunctionRRInConsequent () ((antecedent → (p ↔ q))) (antecedent → ((p ∨ common) ↔ (q ∨ common))))		stmt (buildDisjunctionRRInConsequent () ((antecedent → (p ↔ q))) (antecedent → ((p ∨ common) ↔ (q ∨ common))))
	stmt (buildDisjunctionLLInConsequent () ((antecedent → (p ↔ q))) (antecedent → ((common ∨ p) ↔ (common ∨ q))))		stmt (buildDisjunctionLLInConsequent () ((antecedent → (p ↔ q))) (antecedent → ((common ∨ p) ↔ (common ∨ q))))
		+	stmt (buildConjunctionInConsequent ()
		+	((antecedent → (p0 ↔ q0))
		+	(antecedent → (p1 ↔ q1)))
		+	(antecedent → ((p0 ∧ p1) ↔ (q0 ∧ q1))))
	stmt (buildDisjunctionInConsequent ()		stmt (buildDisjunctionInConsequent ()
	((antecedent → (p0 ↔ q0))		((antecedent → (p0 ↔ q0))

Convenience theorems of propositional logic

Kingdon — Mon, 30 Aug 2010 18:59:43 GMT

add buildConjunctionInConsequent

← Older revision		Revision as of 18:59, 30 August 2010
Line 383:		Line 383:

	var (formula p0 q0 p1 q1)		var (formula p0 q0 p1 q1)
		+	thm (buildConjunctionInConsequent ()
		+	((H0 (antecedent → (p0 ↔ q0)))
		+	(H1 (antecedent → (p1 ↔ q1))))
		+	(antecedent → ((p0 ∧ p1) ↔ (q0 ∧ q1))) (
		+	H0 H1 composeConjunction
		+	p0 q0 p1 q1 ConjunctionFunction
		+	applySyllogism
		+	))
		+
	thm (buildDisjunctionInConsequent ()		thm (buildDisjunctionInConsequent ()
	((H0 (antecedent → (p0 ↔ q0)))		((H0 (antecedent → (p0 ↔ q0)))

Basic arithmetic

Kingdon — Mon, 30 Aug 2010 18:27:38 GMT

add LessThanTotality

← Older revision		Revision as of 18:27, 30 August 2010
Line 1,880:		Line 1,880:
	That gives us <code>a ≤ b ↔ (a ≤ b ∧ a ≠ b) ∨ a = b</code>. But <code>a ≤ b ∧ a ≠ b</code> is just the definition of <code><nowiki><</nowiki></code>, so this is enough.		That gives us <code>a ≤ b ↔ (a ≤ b ∧ a ≠ b) ∨ a = b</code>. But <code>a ≤ b ∧ a ≠ b</code> is just the definition of <code><nowiki><</nowiki></code>, so this is enough.
	<jh>		<jh>
		+	))
		+	</jh>
		+
		+	==== Strict order totality ====
		+	Exactly one of <code><nowiki>a < b</nowiki></code>, <code>a = b</code>, or <code><nowiki>a > b</nowiki></code> holds. We start with the proposition that at least one of the three holds.
		+	<jh>
		+	thm (LessThanTotality () () (((a < b) ∨ (a = b)) ∨ (a > b)) (
		+	</jh>
		+	The meat of the proof is <code>(a < b ∨ a = b) ∨ (b < a ∨ b = a)</code>.
		+	<jh>
		+	a b LessEqualTotality
		+
		+	a b LessEqualLessThan
		+	b a LessEqualLessThan
		+	buildDisjunction
		+
		+	eliminateBiconditionalReverse
		+	applyModusPonens
		+	</jh>
		+	We just need to do some rearranging to finish.
		+	<jh>
		+	swap23ofDisjunction4
		+
		+	b a EqualitySymmetry
		+	(a = b) buildDisjunctionLL
		+
		+	(a = b) DisjunctionIdempotence
		+	swapBiconditional
		+	applyBiconditionalTransitivity
		+
		+	transformDisjunctionRight
		+
		+	swap23ofDisjunction3
	))		))
	</jh>		</jh>

Interface:Classical propositional calculus

Kingdon — Mon, 30 Aug 2010 17:40:43 GMT

add transformDisjunctionRight, swap23ofDisjunction4, swap23ofDisjunction3

← Older revision		Revision as of 17:40, 30 August 2010
Line 507:		Line 507:
	stmt (transformImplicationBiconditionalRight () ((antecedent → (p ↔ q)) (q ↔ r)) (antecedent → (p ↔ r)))		stmt (transformImplicationBiconditionalRight () ((antecedent → (p ↔ q)) (q ↔ r)) (antecedent → (p ↔ r)))
	stmt (transformImplicationDisjunctionLeft () ((antecedent → (p ∨ q)) (p ↔ r)) (antecedent → (r ∨ q)))		stmt (transformImplicationDisjunctionLeft () ((antecedent → (p ∨ q)) (p ↔ r)) (antecedent → (r ∨ q)))
		+	stmt (transformDisjunctionRight () ((p ∨ q) (q ↔ r)) (p ∨ r))
	</jh>		</jh>

Line 515:		Line 516:

	stmt (NegationBiconditional () () ((¬ p) ↔ (p ↔ (⊥))))		stmt (NegationBiconditional () () ((¬ p) ↔ (p ↔ (⊥))))
		+	</jh>
		+
		+	=== Combinations of commutativity and associativity ===
		+	Commutativity and associativity might be combined in any number of ways, but a few patterns turn out to be common.
		+	<jh>
		+	stmt (swap23ofDisjunction4 () (((p ∨ q) ∨ (r ∨ s))) ((p ∨ r) ∨ (q ∨ s)))
		+	stmt (swap23ofDisjunction3 () (((p ∨ q) ∨ r)) ((p ∨ r) ∨ q))
	</jh>		</jh>

Convenience theorems of propositional logic

Kingdon — Mon, 30 Aug 2010 17:38:04 GMT

add transformDisjunctionRight, swap23ofDisjunction4, swap23ofDisjunction3

← Older revision		Revision as of 17:38, 30 August 2010
Line 19:		Line 19:
	As usual, <code>p</code>, <code>q</code>, and <code>r</code> are formulas. We also define some longer names which will make the formulas with a lot of variables more readable.		As usual, <code>p</code>, <code>q</code>, and <code>r</code> are formulas. We also define some longer names which will make the formulas with a lot of variables more readable.
	<jh>		<jh>
-	var (formula p q r antecedent common)	+	var (formula p q r s antecedent common)
	</jh>		</jh>

Line 192:		Line 192:

	applySyllogism		applySyllogism
		+	))
		+
		+	thm (transformDisjunctionRight () ((H (p ∨ q)) (HEQ (q ↔ r))) (p ∨ r) (
		+	H
		+
		+	HEQ
		+	eliminateBiconditionalReverse
		+	p disjoinLL
		+
		+	applyModusPonens
	))		))
	</jh>		</jh>
Line 498:		Line 508:

	applySyllogism		applySyllogism
		+	))
		+	</jh>
		+
		+	== Combinations of commutativity and associativity ==
		+	Commutativity and associativity might be combined in any number of ways, but a few patterns turn out to be common.
		+	<jh>
		+	thm (Disjunction4 () () (((p ∨ q) ∨ (r ∨ s)) ↔ ((p ∨ r) ∨ (q ∨ s))) (
		+	p q (r ∨ s) DisjunctionAssociativity
		+
		+	q r s DisjunctionAssociativity swapBiconditional
		+	p buildDisjunctionLL
		+	applyBiconditionalTransitivity
		+
		+	q r DisjunctionCommutativity
		+	s buildDisjunctionRR
		+	p buildDisjunctionLL
		+	applyBiconditionalTransitivity
		+
		+	r q s DisjunctionAssociativity
		+	p buildDisjunctionLL
		+	applyBiconditionalTransitivity
		+
		+	p r (q ∨ s) DisjunctionAssociativity swapBiconditional
		+	applyBiconditionalTransitivity
		+	))
		+
		+	thm (swap23ofDisjunction4 () ((H ((p ∨ q) ∨ (r ∨ s)))) ((p ∨ r) ∨ (q ∨ s)) (
		+	H
		+	p q r s Disjunction4
		+	eliminateBiconditionalReverse
		+	applyModusPonens
		+	))
		+
		+	thm (Disjunction3 () () (((p ∨ q) ∨ r) ↔ ((p ∨ r) ∨ q)) (
		+	p q r DisjunctionAssociativity
		+
		+	q r DisjunctionCommutativity
		+	p buildDisjunctionLL
		+	applyBiconditionalTransitivity
		+
		+	p r q DisjunctionAssociativity
		+	swapBiconditional
		+	applyBiconditionalTransitivity
		+	))
		+
		+	thm (swap23ofDisjunction3 () ((H ((p ∨ q) ∨ r))) ((p ∨ r) ∨ q) (
		+	H
		+	p q r Disjunction3
		+	eliminateBiconditionalReverse
		+	applyModusPonens
	))		))
	</jh>		</jh>

Basic arithmetic

Kingdon — Mon, 30 Aug 2010 17:00:47 GMT

add some definitions, LessEqualLessThan

← Older revision		Revision as of 17:00, 30 August 2010
(One intermediate revision not shown)
Line 1,811:		Line 1,811:
	a a LessEqualTotality		a a LessEqualTotality
	conflateDisjunction		conflateDisjunction
		+	))
		+	</jh>
		+
		+	Equality implies <code>≤</code>.
		+	<jh>
		+	thm (EqualityLessEqual () () ((a = b) → (a ≤ b)) (
		+	a LessEqualReflexivity
		+
		+	a b a LessEqualBuilderLL
		+	</jh>
		+	The builder gives us <code>a = b → (a ≤ a ↔ a ≤ b)</code>. But <code>a ≤ a</code> is a theorem, so we are done.
		+	<jh>
		+	detachImplicationBiconditional
		+	))
		+	</jh>
		+
		+	==== Strict order ====
		+	Here we define <code><nowiki><</nowiki></code>, as well as <code><nowiki>></nowiki></code> and <code>≥</code>.
		+	<jh>
		+	def ((< a b) ((a ≤ b) ∧ (a ≠ b)))
		+	def ((> b a) (a < b))
		+	def ((≥ b a) (a ≤ b))
		+	</jh>
		+
		+	We next prove <code>a ≤ b ↔ a < b ∨ a = b</code> (finally justifying the informal name "less than or equal to" for <code>≤</code>). The proof is fairly straightforward expansion of the definition and rearrangement, but it will be easier to break out part of the proof into a lemma.
		+	<jh>
		+	thm (LessEqualLessThanLemma () () ((a ≤ b) ↔ (((a ≤ b) ∨ (a = b)) ∧ ((a ≠ b) ∨ (a = b)))) (
		+	</jh>
		+	We start with the forward implication. The first half is <code>a ≤ b → a ≤ b ∨ a = b</code>
		+	<jh>
		+	(a ≤ b) (a = b) DisjunctionRightIntroduction
		+	</jh>
		+	The second half is <code>a ≤ b → a ≠ b ∨ a = b</code>
		+	<jh>
		+	(a = b) TertiumNonDatur swapDisjunction
		+	(a ≤ b) introduceAntecedent
		+	</jh>
		+	Combining these gives us the forward implication.
		+	<jh>
		+	composeConjunction
		+	</jh>
		+	Moving on to the reverse implication, we start with <code>(a ≤ b ∨ a = b) ∧ (a ≠ b ∨ a = b) → a ≤ b ∨ a = b</code>
		+	<jh>
		+	((a ≤ b) ∨ (a = b)) ((a ≠ b) ∨ (a = b)) ConjunctionRightElimination
		+	</jh>
		+	Then we show <code>a ≤ b ∨ a = b → a ≤ b</code>.
		+	<jh>
		+	(a ≤ b) ImplicationReflexivity
		+	a b EqualityLessEqual
		+	composeDisjunction
		+	</jh>
		+	Combining these gives the reverse implication,
		+	<jh>
		+	applySyllogism
		+	</jh>
		+	and combining forward and reverse implications completes the proof.
		+	<jh>
		+	introduceBiconditionalFromImplications
		+	))
		+
		+	thm (LessEqualLessThan () () ((a ≤ b) ↔ ((a < b) ∨ (a = b))) (
		+	a b LessEqualLessThanLemma
		+
		+	(a ≤ b) (a ≠ b) (a = b) DisjunctionRightDistribution
		+	swapBiconditional
		+	applyBiconditionalTransitivity
		+	</jh>
		+	That gives us <code>a ≤ b ↔ (a ≤ b ∧ a ≠ b) ∨ a = b</code>. But <code>a ≤ b ∧ a ≠ b</code> is just the definition of <code><nowiki><</nowiki></code>, so this is enough.
		+	<jh>
	))		))
	</jh>		</jh>