by Hugh McGuire
gcd()
and mod),
functions such as log2(),
sets, summations,
time complexity (O(), Θ(), etc.),
and counting (combinatorics).
As with other systems,
ProofBuilder covers a wide range of formal reasoning,
from propositional
simplification to strong induction;
but what the author hopes distinguishes ProofBuilder is
that it is designed to enable users to do proofs as much as possible
like the way they might otherwise do them manually.
Such aspects of the design include a
framework that clarifies which formulas in a proof are premises that are
hypothesized to be true, and which are goal formulas that need to be
proven; and mechanisms to apply a variety of proof methods and strategies
such as forward and backward reasoning, proving by contradiction, and
proving by cases.
For an illustration, here is a sample proof constructed using ProofBuilder:
http://www.cis.gvsu.edu/~mcguire/ProofBuilder/The subfolders/subdirectories there and their contents are as follows:
- download/
- This subfolder/subdirectory contains ProofBuilder.jar .
- manual/
- This subfolder/subdirectory contains a manual for ProofBuilder.
- summary.ppt
- This PowerPoint document summarizes how ProofBuilder works — including a very brief summary of instructions for using it.
- samples/
- This subfolder/subdirectory contains sample proofs done in ProofBuilder.
- presentations/
- This subfolder/subdirectory contains presentations or publications about ProofBuilder.
- src/
- This subfolder/subdirectory contains the source code for ProofBuilder.
java -ea -jar ProofBuilder.jar
If downloading
ProofBuilder.jar
actually created the file "ProofBuilder.zip",
then try the following command instead:
java -ea -jar ProofBuilder.zip
ProofBuilder's main window — the second of the two windows shown immediately above — contains first (at the top) four menus with the following titles: "ProofBuilder", "System", "Management", and "Deduction". Below that menu bar is an area for a proof structured as a "deductive tableau", which is a table with five columns as follows: two main columns labeled "Suppositions and derivations" and "Theorem and subgoals", containing the logic formulas used in the proof (and also some narrative texts); a column labeled "Used" containing check boxes indicating whether formulas have been used yet in the proof; and two columns labeled "(#)" and "Comments" containing numbers and descriptions for identifying logic formulas.
After you enter the theorem (and presuppositions, if any),
you use the mouse to select expressions
and
use the Deduction menu to choose deductive
operations
for ProofBuilder
to apply to
the selected expressions;
then, ProofBuilder adds the results of your deductions to the proof.
The proof is finished
when you achieve a goal of true
(or a supposition/derivation of false,
say if you're doing a proof by contradiction or using resolution).
While you are entering expressions here, you can do editing as usual: double-clicking the mouse to select a word, pressing arrow keys ("←", "↑", "↓", and "→" on your keyboard) to navigate around in the text, etc. You can navigate around in the text also by using the following keystrokes (which are derived from other systems such as emacs):
You can also use standard keyboard shortcuts for editing actions — including pasting texts copied from different sources (Web pages, PDF documents, Microsoft Word documents, etc.):
keystroke action ctrl-b move backward one character (←) ctrl-p move upward one line (↑) ctrl-n move downward one (next) line (↓) ctrl-f move forward one character (→) ctrl-h erase one character backward (backspace) ctrl-j insert line break (return/enter)
A caveat about copying/pasting is that some characters such as "∀" (forall) or "(On an Apple Macintosh computer, you may need to use the key "⌘" ("command") instead of the key "ctrl".)
keystroke action ctrl-x cut ctrl-c copy ctrl-v paste ctrl-a select all
-" (superscript minus)
may not transfer correctly,
so pasting may yield a few incorrect characters
which may
show up
as
unsuperscripted when they're supposed to be superscripted,
or
as multiple letters with accents
when they're supposed to be
individual
mathematical symbols, or other
differences
like that.
In such cases, you may need to manually replace any incorrect characters
which you may see
with the correct ones that you intended.
The symbols that you can enter in ProofBuilder are shown in the two tables following this paragraph. For a symbol that you can't type straightforwardly using a standard keyboard, e.g. "∧" or "∀", the second table's second column headed "alt key" indicates that you can press the key alt and the specified regular key to enter the symbol. For example, you can press alt and a to enter the symbol "&and"; and you can press alt and A (shift-a) to enter the symbol "∀". (The user-entry window also shows this information about which special symbols can be entered by pressing alt and regular keys.) On some platforms such as Apple Macintoshes, you may need to press ctrl in addition to "alt" etc. Further, you can enter a special symbol by clicking on it where it's shown below the entry area. And finally, remember that you can copy/paste special symbols from different documents — including this manual.
Note: Microsoft's Web-browser Internet Explorer may not properly render characters here such as "∧" and "∀". If necessary, click here to access a version of this document in PDF instead of HTML. Or, alternatively, try another Web-browser, e.g. Mozilla Firefox, which is free.
symbol how to type purpose example of use integeroptional "-" followed
by adjacent digitsnumeric value 42identifierletter followed by
adjacent letters/
digits/underscorespredicate or function or
variable or constantIsParent
symbol alt key name example of use )right parenthesis (3 + 4)·5]right bracket [(3 + 4)·5]⁶}right brace {1,2,3,4}|right bar delimiter |{1,2,3,4}|⌋right floor ⌊5/3⌋ = 1⌉right ceiling ⌈5/3⌉ = 2(left parenthesis (3 + 4)·5[left bracket [(3 + 4)·5]⁶{left brace {1,2,3,4}|left bar delimiter |{1,2,3,4}|⌊left floor ⌊5/3⌋ = 1⌈left ceiling ⌈5/3⌉ = 2∀A universal quantifier ∀x[x < x + 1]foralluniversal quantifier (forall x)[x < x + 1]FORALLuniversal quantifier (FORALL x)[x < x + 1]∃E existential quantifier ∃y[x < y]existsexistential quantifier (exists y)[x < y]EXISTSexistential quantifier (EXISTS y)[x < y]forsomeexistential quantifier (forsome y)[x < y]FORSOMEexistential quantifier (FORSOME y)[x < y]∑S summation (∑ 1/2^i for i=0 to ∞) = 2∏P product (∏ 2^i for i=1 to 8) = 2^36≡= equivalence/biconditional (x < y) ≡ (y > x)⇔B equivalence/biconditional (x < y) ⇔ (y > x)<==>equivalence/biconditional (x < y) <==> (y > x)↔b equivalence/biconditional (x < y) ↔ (y > x)<-->equivalence/biconditional (x < y) <--> (y > x)iffequivalence/biconditional (x < y) iff (y > x)IFFequivalence/biconditional (x < y) IFF (y > x)equivequivalence/biconditional (x < y) equiv (y > x)EQUIVequivalence/biconditional (x < y) EQUIV (y > x)⇒I implication (x < y) ⇒ (x ≤ y)==>implication (x < y) ==> (x ≤ y)→i implication (x < y) → (x ≤ y)-->implication (x < y) --> (x ≤ y)⊃j implication (x < y) ⊃ (x ≤ y)impliesimplication (x < y) implies (x ≤ y)IMPLIESimplication (x < y) IMPLIES (x ≤ y)∨o disjunction/or (x < y) ∨ (x ≥ y)\/disjunction/or (x < y) \/ (x ≥ y)ordisjunction/or (x < y) or (x ≥ y)ORdisjunction/or (x < y) OR (x ≥ y)∧a conjunction/and (3 < 4) ∧ (4 < 5)/\conjunction/and (3 < 4) /\ (4 < 5)andconjunction/and (3 < 4) and (4 < 5)ANDconjunction/and (3 < 4) AND (4 < 5)≅~ congruence 8 ≅ 3 (mod 5)≡= congruence 8 ≡ 3 (mod 5)=equals 1 + 1 = 2ishas order 3n+5 is Θ(n):=becomes x := 2←: becomes x ← 2becomesbecomes x becomes 2BECOMESbecomes x BECOMES 2≠# inequality/different 3 ≠ 4neqinequality/different 3 neq 4NEQinequality/different 3 NEQ 4≤< less than or equal to 3 ≤ 4leqless than or equal to 3 leq 4LEQless than or equal to 3 LEQ 4≥> greater than or equal to 5 ≥ 4geqgreater than or equal to 5 geq 4GEQgreater than or equal to 5 GEQ 4<less than 3 < 4>greater than 5 > 4|divides 3|18dividesdivides 3 divides 18DIVIDESdivides 3 DIVIDES 18∈e element of / is in x ∈ S∉r not an element of x ∉ ∅⊂c proper subset of S1 ⊂ S2subsetproper subset of S1 subset S2SUBSETproper subset of S1 SUBSET S2⊆C subset of or equal to S1 ⊆ S2subseteqsubset of or equal to S1 subseteq S2SUBSETEQsubset of or equal to S1 SUBSETEQ S2,comma f(x,y)forrange specification (∑ 1/2^i for i=0 to ∞) = 2FORrange specification (∑ 1/2^i FOR i=0 TO ∞) = 2torange separator (∑ 1/2^i for i=0 to ∞) = 2TOrange separator (∑ 1/2^i FOR i=0 TO ∞) = 2modmodulo a mod m∪u union S1 ∪ S2unionunion S1 union S2UNIONunion S1 UNION S2∩t intersection S1 ∩ S2intersectintersection S1 intersect S2INTERSECTintersection S1 INTERSECT S2+addition 3 + 4-subtraction 3 - 4/quotient 3/4·. multiplication 3·4*multiplication 3*4<adjacency>multiplication 3n^exponentiation x^y`exponentiation x`yexpexponentiation x exp yEXPexponentiation x EXP y'prime x'!factorial 4! = 4·3·2·1⁰0 superscript zero x⁰ = 1¹1 superscript one x¹ = x²2 superscript two x² = x·x³3 superscript three x³ = x·x·x⁴4 superscript four x⁴ = x·x³⁵5 superscript five x⁵ = x·x⁴⁶6 superscript six x⁶ = x·x⁵⁷7 superscript seven x⁷ = x·x⁶⁸8 superscript eight x⁸ = x·x⁷⁹9 superscript nine x⁹ = x·x⁸-- superscript minus x · x-1 = 1-negative -(3 + 4)lnnatural logarithm base e (2.71828...) ln(1) = 0log10logarithm base ten log10(1000) = 3lglogarithm base two lg(128) = 7loglogarithm lg(x) = log(2,x)ΘO same order 3n + 5 is Θ(n)ΩW lower bound 3n²+5 is Ω(n)ωw strict lower bound 3n²+5 is ω(n)~complement ~S¬n not ∀x[¬(x < x)]'not ∀x[(x < x)']notnot ∀x[not (x < x)]NOTnot ∀x[NOT (x < x)].quantifier separator (OPTIONAL) ∃x.P(x)@substitution (2*i+1)@[i:=n+1] = 2*(n+1)+1◀@ substitution (2*i+1)◀[i:=n+1] = 2*(n+1)+1∞y infinity (∑ 1/2^i for i = 0 to ∞) = 2ℝR real numbers (∃x)[x ∈ ℝ ∧ x² = 2]ℚQ rational numbers 8/3 ∈ ℚℤZ integer numbers -7 ∈ ℤℕN natural numbers 0 ∈ ℕ∅/ empty set x ∉ ∅truetrue x = x ⇔ trueTRUEtrue x = x ⇔ TRUEfalsefalse x = x + 1 ⇔ falseFALSEfalse x = x + 1 ⇔ FALSE
The relative precedences
of operators that take arguments
are given by their order in the preceding list,
from weakest precedence at the beginning
to strongest precedence at the end —
except
that "+" and binary "-"
have equal precedence.
For example,
the expression "3 + 4 * 5"
is interpreted
as "3 + (4 * 5)",
and
the expression "P ∧ Q ∨ R"
is interpreted
as "(P ∧ Q) ∨ R".
Most of the binary operators here have left associativity;
ones that instead have right associativity
include implication and exponentiation.
For example,
the expression "3 - 4 - 5"
is interpreted
as "(3 - 4) - 5",
the expression "P ⇒ Q ⇒ R"
is interpreted
as "P ⇒ (Q ⇒ R)",
and
the expression "2^2^n"
is interpreted
as "2^(2^n)".
You might not really notice it, but
multiplication is handled slightly differently here than
the way it is in
programming languages.
For one thing,
the precedence of multiplication here is actually stronger than
the precedence of division;
thus,
for example, the
expression "x/3y"
is understood
as "x/(3y)"
rather than "(x/3)·y".
Another difference is that multiplication here
has right associativity
instead of left associativity;
thus,
for example,
the
expression "3n(n+1)"
is understood
as "3·[n·(n+1)]"
rather than "(3·n)·(n+1)".
You can use space characters, tab characters, and newline characters to separate symbols as you may need or desire, e.g. in "P implies Q".
You can use the newline character as a grouping delimiter, e.g. as follows:
3 + 4 - 5
*
6 - 7 + 8
That material is interpreted as "(3 + 4 - 5) * (6 - 7 + 8)".
Another example is as follows:
(P ∨ Q) ⇒ R
⇒
(P ⇒ R) ∧ (Q ⇒ R)
That material is interpreted
as "[(P ∨ Q) ⇒ R] ⇒ [(P ⇒ R) ∧ (Q ⇒ R)]".
/* ... */
// ... to end of line
(<digits>) to end of line
"..."
For examples:
If the material that you entered is OK, then ProofBuilder closes the user-entry window and adds the formula(s) that you entered into the proof as follows: presuppositions are placed in the Suppositions/derivations column, in the deductive tableau's first rows (naturally, in the order in which you entered them); and the theorem to be proved is placed in the Theorem/subgoals column, in the first row following the presuppositions (if any). For example, here is a sequence of images showing entry of a theorem to prove and presuppositions to be used in the proof:
1 + 2" to "3",
the formula "4 < 9" to "true",
and
the term "55 mod 7" to "6".
A more 'generic' example is that
ProofBuilder simplifies any expression of the
form "0 + τ" to "τ",
where "τ" can be any arithmetic term.
Another generic example
is that
when an equation
has the form "τ = τ",
where the term τ
on the left side of the "="
is identical to the term on the right side,
then
ProofBuilder simplifies the equation to true.
And similarly,
ProofBuilder simplifies the
formula "τ ≠ τ" to "false".
ν"
stands for any variable,
and the
abbreviations "f"
and "t"
are used
for "false"
and "true",
respectively.
(The symbols "∧", "∨", "→", and "↔"
are used in the presentation here of the rewritings,
but you can actually use other symbols
such as "AND", "\/kbd>", "⇒", and "iff"
that are available for these operators —
see Section 3.2
above regarding
options for typing mathematical symbols.
See also
the additional notes
regarding this issue.)
f ∧ φ------> ft ∧ φ------> φφ ∧ φ------> φφ ∧ ¬φ------> ff ∨ φ------> φt ∨ φ------> tφ ∨ φ------> φφ ∨ ¬φ------> tf → φ------> tt → φ------> φφ → φ------> tφ → ¬φ------> ¬φφ → f------> ¬φφ → t------> tφ → φ------> t¬φ → φ------> φ
¬¬φ------> φ¬φ1 → ¬φ2------> φ2 → φ1¬(φ1 → ¬φ2)------> φ1 ∧ φ2
∀ν[φ]------> φif νis not a free variable inφSee also Section 7.4 below regarding rewritings which you can apply to logic formulas as you may desire. ∃ν[φ]------> φif νis not a free variable inφYou can do other, algebraic manipulations by applying equations as indicated in Section 7.2 below.
4. The ProofBuilder menu
The ProofBuilder menu contains the following items:About ProofBuilder View copyright and license (etc.) Quit ProofBuilder ^⇧QThe annotation "^⇧Q" at right above specifies a combination of keys which you can press as a shortcut to activate the menu item Quit ProofBuilder: "^" represents the key ctrl, and "⇧" represents the key shift, so "^⇧Q" represents the key-combination <ctrl-shift-Q>.The following subsections describe the functionalities of each of these menu items.
4.1. The About ProofBuilder menu item
If you choose this menu item, then ProofBuilder will display basic information about its version and the author.4.2. The View copyright and license (etc.) menu item
If you choose this menu item, then ProofBuilder will display copyright and license information.4.3. The Quit ProofBuilder menu item
If you choose this menu item, then ProofBuilder will quit. Except if you haven't saved your current proof since you last modified it, then ProofBuilder will display a dialog window asking whether you really want to discard your modified proof without having saved it, as follows:If you choose Yes here by pressing Enter or space on your keyboard or by clicking the Yes button with your mouse, then ProofBuilder will discard your current proof and quit. If you choose the No button here instead, then ProofBuilder won't discard your current proof and it won't quit.
5. The System menu
The System menu contains the following items:New proof ^⇧N Update username Save as Web page ^⇧S Save in native-format file Reopen native-format file Copy selected (sub)expression to clipboard ^⇧C About printingThe annotations at right above of the form "^⇧X" specify combinations of keys which you can press as shortcuts to activate the menu items that have them: "^" represents the key ctrl and "⇧" represents the key shift, so "^⇧X" represents the keystroke <ctrl-shift-X>, when X is an appropriate character (N, S, or C here).The following subsections describe the functionalities of each of these menu items:
5.1. The New proof menu item
If you choose this menu item, then ProofBuilder will discard your current proof and start a new one, displaying the user-entry window for you to enter the theorem for your new proof. Except if you haven't saved your current proof since you last modified it, then ProofBuilder will display a dialog window asking whether you really want to discard your modified proof without having saved it, as follows:If you choose Yes here by pressing Enter or space on your keyboard or by clicking the Yes button with your mouse, then ProofBuilder will proceed to discard your current proof and start a new proof. If you choose the No button here instead, then ProofBuilder won't discard your current proof and it won't start a new proof.
5.2. The Update username menu item
This menu item enables you to update your username in case ProofBuilder may not be able to otherwise determine it correctly. (For example, in one system ProofBuilder always used the default username "labuser".)5.3. The Save as Web page menu item
As this menu item's name indicates, you can employ it to save your proof as a Web page (in HTML).5.4. The Save in native-format file menu item
As this menu item's name indicates, you can employ it to save your proof in a file using a format that is 'native' i.e. internal to ProofBuilder, so you could later reopen the file and continue the proof.5.5. The Reopen native-format file menu item
This menu item enables you to reload a partial (or complete) proof which you worked on and saved previously in native format.Note: This menu item does not enable you to reload a partial (or complete) proof that you worked on and saved previously as a Web page in HTML. If you want to reload such a proof, then try doing the following: Use a Web browser to open your partially (or fully) completed proof that you saved as a Web page in HTML, copy the theorem and presuppositions (if any) from there and paste them into ProofBuilder, and then redo the deductive steps that your original proof shows you did previously. (It should be easy to redo deductions when you already know what to do; what's hard generally is determining what to do in the first place! ;-)
5.6. The Copy selected (sub)expression to clipboard menu item
As this menu item's name indicates, you can employ it to copy an expression which you have selected in your proof to your system clipboard, so you can reproduce it (elsewhere) using 'paste'.5.7. The About printing menu item
As this menu item's name indicates, you can employ it to view information about printing, as follows:To print a proof produced by ProofBuilder, use the Save as Web page menu item,
and then use a Web browser to open and print the Web page containing your proof.
(Web browsers provide more options for handling output — changing paper orientation, changing
font size, 'printing' to a PDF file instead of really to a printer, etc. — than ProofBuilder might.)
6. The Management menu
The Management menu contains the following items:Enter theorem Add presuppositions ^P Increase font size ^⇧- Decrease font size ^- Use ~ for NOT Use ′ for NOT Delete highest numbered step ^⇧DThe notations of the forms "^X" and "^⇧X" specify combinations of keys which you can press as shortcuts to activate the menu items that have them: "^" represents the key ctrl and "⇧" represents the key shift, so for examples "^P" represents the keystroke <ctrl-P> and "^⇧D" represents the keystroke <ctrl-shift-D>.The following subsections describe the functionalities of each of these menu items:
6.1. The Enter theorem menu item
As this menu item's name indicates, you can employ it to enter a theorem to be proved (if you haven't done that yet). If you choose this menu item, then ProofBuilder displays the user-entry window which is described above in Section 3, so you can enter material as you may desire.6.2. The Add presuppositions menu item
As this menu item's name indicates, you can use it to enter presuppositions such as axioms or lemmas into your proof. If you choose this menu item, then ProofBuilder displays the user-entry window which is described above in Section 3, so you can enter material as you may desire.6.3. The Increase font size menu item
As this menu item's name indicates, you can use it to increase the sizes of the symbols that ProofBuilder displays.6.4. The Decrease font size menu item
As this menu item's name indicates, you can use it to decrease the sizes of the symbols that ProofBuilder displays.6.4. The Use ~ for NOT menu item
As this menu item's name indicates, you can use it to instruct ProofBuilder to use the symbol "~" for NOT.6.4. The Use ′ for NOT menu item
As this menu item's name indicates, you can use it to instruct ProofBuilder to use the symbol "′" for NOT.6.7. The Delete highest numbered step menu item
As this menu item's name indicates, you can choose it to delete the highest numbered step in your proof. This provides a primitive way for you to discard parts of a proof that you decide you don't want.
7. The Deduction menu
The Deduction menu contains the following items:Transform one side to the other ^T Apply equation or equivalence ^E Apply comparison ("<", "≤", ">", or "≥") ^L (mnemonic: "L" somewhat like "<") Rewrite logical expression ^R Split row's formula ^S Invoke bivalence for a proposition ^B Apply one formula to another matching one ^M (a.k.a. modus ponens etc.) Assign a value to the selected variable ^⇧A Remove quantifier ^Q Invoke induction ^I Suppose negation ^N Conjoin two suppositions/derivations ^⇧J Introduce existential quantifier "∃" ^⇧E Introduce univeral quantifier "∀" ^⇧U Try simplificationThe annotations of the forms "^X" and "^⇧X" at right above specify combinations of keys which you can press as shortcuts to activate the menu items that have them: "^" represents the key ctrl and "⇧" represents the key shift, so for examples "^T" represents the key-combination <ctrl-T> and "^⇧I" represents the key-combination <ctrl-shift-I>.Subsection 7.0 here describes arrangements that are common for several of these deductive actions. Then, Subsections 7.1ff. below describe the specific functionalities of each of these menu items.
Note: Microsoft's Web-browser Internet Explorer may not properly render characters here such as "∧" and "∀". If necessary, click here to access a version of this document in PDF instead of HTML. Or, alternatively, try another Web-browser, e.g. Mozilla Firefox, which is free.7.0. Arrangements for deductive actions
7.0.1. Selecting Expressions
To apply deductive actions, you need to select expressions. Clicking on a row containing an expression initially selects the entire expression in the row. To select a subexpression, use your mouse/cursor to drag through it (while doing such dragging, you generally don't need to be that precise about reaching the endpoints of the subexpression: ProofBuilder infers what endpoints you intend). Or, find the main operator ("∧" or "+" or whatever) of the subexpression that you want to select and use your mouse/cursor to select that operator as you would usually select a word when you do GUI editing, by dragging your mouse/cursor through it or double-clicking it or slowly single-clicking it.You can arrange for multiple rows to be selected — again as usual when you do GUI editing — by holding down a key such as ctrl or ⌘ while clicking.
7.0.2. Polarities
Some of the deductive actions depend on an attribute called "polarity" which is ascribed to logic formulas and subformulas. As with magnetism, the values for polarity here include "North", which is abbreviated as "N", and "South", which is abbreviated as "S". But one further possibility here is that a formula or subformula can possess both of the polarities North and South; this is denoted with the polarity "Both", which is abbreviated as "B". Then, a formula or subformula can have the polarity North by having just North or by having Both (North and South); and a formula or subformula can have the polarity South by having just South or by having Both (South and North). A formula or subformula has strictly North polarity if it has only the polarity North, not Both (i.e. not also South); and a formula or subformula has strictly South polarity if it has only the polarity South, not Both (i.e. not also North). Another detail is that the polarities North and South are considered opposites of each other; and the polarity Both is considered the opposite of itself (because the polarity Both may be considered as the set {North,South}, and taking opposites for those values respectively yields the set {South,North}, which is Both again because with sets, {South,North} = {North,South}).Polarities for formulas and subformulas in a deductive tableau are determined as follows: To begin, each outermost supposition formula has South polarity, and each outermost goal formula has North polarity — a goal formula needs to be proven. Then, inner subformulas' polarities are determined as follows:
- If a formula
φis a quantification, i.e.φhas the form "∀ν[σ]" or "(∃ν)[σ]"; or ifφis a conjunction, i.e.φhas the form "σ1 ∧ σ2"; or ifφis a disjunction, i.e.φhas the form "σ1 ∨ σ2"; then in any such case, each subformulaσorσ1orσ2has the same polarity as the outer formulaφ.
- If a formula
φis a negation, i.e.φhas the form "¬σ", then the polarity of the subformulaσis the opposite of the polarity of the outer formulaφ. For example if the formula¬Phas North polarity, then the subformulaPinside there has South polarity.
- If a formula
φis an implication, i.e.φhas the form "σ1 → σ2", then the polarity of the subformulaσ1is the opposite of the polarity of the outer formulaφhere, and the polarity of the subformulaσ2is the same as the polarity of the outer formulaφhere. For example if the formula(P → Q)has South polarity, then the subformulaPinside there has North polarity and the subformulaQinside there has South polarity.
- If a formula
φis an equivalence, i.e.φhas the form "σ1 ↔ σ2", then the subformulasσ1andσ2each have Both polarities (i.e., they each have both North and South polarities.) For example with the formula(P ↔ Q), no matter what may be the polarity of the outer formula here, the subformulaPhere has Both polarities and the subformulaQhere has Both polarities.7.1. Transform one side to the other
You can use this menu item to prove a goal formula that is an equation (of the form "τ1 = τ2") or an equivalence (of the form "φ1 ↔ φ2" or "φ1 ⇔ φ2" or "φ1 ≡ φ2" or "φ1 iff φ2"), e.g. as follows (also demonstrating the deduction Apply equation or equivalence):Here is a second example, for the equivalence operator "
↔", a.k.a. "⇔" or "≡" or "iff" (again demonstrating the deduction Apply equation or equivalence also):Proof of the following formula:And here is a third example, for "A ∪ ∅ = A
(#) Suppositions and derivations Theorem and subgoals We presuppose the following: (1) (2) (3) We start working with the formula being proved
as follows:(4) ≡ by (1) with " S1 := A∪∅, S2 := A"(5) Well, let an arbitrary value " a" be given;
then we should prove the following:(6) We'll work on transforming the left-hand side of formula (6)
to the right-hand side as follows:(7) ≡ by (2) with " x := a, S1 := A, S2 := ∅"(8) ↓ by (3) with " x := a"(9) ≡ by simplifying (10) And that satisfies the earlier goal (6); i.e. we have: (11) That concludes this part of the proof. Thus, the theorem that was given is true. ≤" (less-than-or-equal), also demonstrating the deduction Apply comparison ("<", "≤", ">", or "≥") (note: this is a simplified version of a larger proof with the condition1 ≤ n):Proof of the following formula:The first sample proof in Section 7.10 (Invoke induction) below provides an example of transforming the right-hand side of an equation to the left-hand side; this is done following row (13) there.(∃c)[2·n + 5 ≤ c·(n²)]
(#) Suppositions Theorem/Subgoals We presuppose the following: (1) (2) We start working with the formula being proved
as follows:(3) Removing that variable quantification
clarifies that to prove that formula,
it will suffice to find a value for the variable.(4) Instantiating " z" with "5" in formula (2) yields:(5) ≡ by simplifying (6) We'll work on transforming the left-hand side of formula (4)
to the right-hand side as follows:(7) ≤ by (1) (8) ≤ by (6) (9) = by simplifying (10) And that satisfies our earlier goal (4)
with "c := 7"; i.e. we have:(11) That concludes this part of the proof. Thus, the theorem that was given is true.
7.2. Apply equation or equivalence
This deductive action enables you to replace an expression which you have selected with an equal or equivalent one, according to an equation ("τ1 = τ2") or an equivalence ("φ1 ↔ φ2" or "φ1 ⇔ φ2" or "φ1 ≡ φ2" or "φ1 iff φ2") which you have also selected. The equation or equivalence that you use here needs to have South polarity (because otherwise deduction might be unsound, i.e. you might be able to prove things that aren't really true; see the additional notes for more information regarding this issue). Two sample proofs using this deduction are presented in the preceding subsection (7.1 Transform one side to the other); here is another example:Proof of the following formula:C(n+1,k+1) = [(n+1)/(k+1)]·C(n,k)
(#) Suppositions and derivations Theorem and subgoals We presuppose the following: (1) (2) (3) (4) We start working with the formula being proved
as follows:(5) We'll work on transforming the left-hand side of formula (5)
to the right-hand side as follows:(6) = by (1) with " x := n+1, y := k+1"(7) = by simplifying (8) = by (2) with " x := n"(9) = by (2) with " x := k"(10) = by (3) with " x := k+1, y := k!, z := (n-k)!"(11) = by (4) with " w := n+1, y := n!, x := k+1, z := k!·(n-k)!"(12) = by (1) with " x := n, y := k"(13) And that satisfies our earlier goal (5); i.e. we have: (14) That concludes this part of the proof. Thus, the theorem that was given is true.
7.3. Apply comparison ("<", "≤", ">", or "≥")
This deductive action enables you to replace one expression which you have selected with another one that is smaller or larger (or maybe equal) according to an inequality — "τ1 < τ2" or "τ1 ≤ τ2" or "τ1 > τ2" or "τ1 ≥ τ2" — which you have also selected. The inequality that you use here needs to have South polarity (because otherwise deduction might be unsound, i.e. you might be able to prove things that aren't really true; see the additional notes for more information regarding this issue). A sample proof using this deduction is presented in the earlier subsection 7.1 Transform one side to other; here is another example:Proof of the following formula:a < c
(#) Suppositions and derivations Theorem and subgoals We presuppose the following: (1) (2) We start working with the formula being proved
as follows:(3) We'll work on transforming the left-hand side of formula (3)
to the right-hand side as follows:(4) ≤ by (1) (5) < by (2) (6) And that satisfies our earlier goal (3); i.e. we have: (7) That concludes this part of the proof. Thus, the theorem that was given is true.
7.4. Rewrite logical expression
Note: Microsoft's Web-browser Internet Explorer may not properly render characters here such as "∧" and "∀". If necessary, click here to access a version of this document in PDF instead of HTML. Or, alternatively, try another Web-browser, e.g. Mozilla Firefox, which is free.
This menu item enables you to rewrite a logic formula or subformula which you have selected in various ways, as indicated by the following table of rewritings.For each rewriting, the left side can be rewritten to the right side or vice-versa. Although it's redundant, each rewriting is listed here each way to help you look up all the different rewritings that can apply to a formula with a particular operator that you are considering. The symbols "φ", "φ1", "φ2", and "φ3" stand for any logic formulas, and the symbols "
ν", "ν1", and "ν2" stand for any variables. (The symbols "∧", "∨", "⇒", and "⇔" are used in the presentation here of the rewritings, but you can actually use other symbols that are available for these operators — see Section 3.2 above regarding options for typing mathematical symbols. See also the additional notes regarding this.)These rewritings do not include simplifications, which are performed automatically; see Section 3.7 above.
rewriting name (if any) ¬(φ1 ∧ φ2) ↔ ¬φ1 ∨ ¬φ2 DeMorgan's Law for "¬∧" ¬(φ1 ∨ φ2) ↔ ¬φ1 ∧ ¬φ2 DeMorgan's Law for "¬∨" ¬(φ1 ⇒ φ2) ↔ φ1 ∧ ¬φ2 not implies ¬(φ1 ⇔ φ2) ↔ φ1 ⇔ ¬φ2 not iff ¬(∃ν)[φ] ↔ (∀ν)[¬φ] Generalized DeMorgan's Law
a.k.a. ∀ and ∃ are inverses¬(∀ν)[φ] ↔ (∃ν)[¬φ] Generalized DeMorgan's Law
a.k.a. ∀ and ∃ are inverses¬φ1 ∧ ¬φ2 ↔ ¬(φ1 ∨ φ2) DeMorgan's Law (for "¬∨") φ1 ∧ ¬φ2 ↔ ¬(φ1 ⇒ φ2) φ1 ∧ (φ2 ∨ φ3) ↔ (φ1 ∧ φ2) ∨ (φ1 ∧ φ3) distributivity of "∧" over "∨" (φ1 ∨ φ2) ∧ (φ1 ∨ φ3) ↔ φ1 ∨ (φ2 ∧ φ3) distributivity (of "∨" over "∧") (φ1 ⇒ φ2) ∧ (φ2 ⇒ φ1) ↔ φ1 ⇔ φ2 φ1 ∧ φ2 ↔ φ2 ∧ φ1 commutativity of "∧" φ1 ∧ (φ2 ∧ φ3) ↔ (φ1 ∧ φ2) ∧ φ3 associativity of "∧" (φ1 ∧ φ2) ∧ φ3 ↔ φ1 ∧ (φ2 ∧ φ3) associativity of "∧" ¬φ1 ∨ ¬φ2 ↔ ¬(φ1 ∧ φ2) DeMorgan's Law (for "¬∧") ¬φ1 ∨ φ2 ↔ φ1 ⇒ φ2 φ1 ∨ (φ2 ∧ φ3) ↔ (φ1 ∨ φ2) ∧ (φ1 ∨ φ3) distributivity of "∨" over "∧" (φ1 ∧ φ2) ∨ (φ1 ∧ φ3) ↔ φ1 ∧ (φ2 ∨ φ3) distributivity (of "∧" over "∨") (φ1 ∧ φ2) ∨ (¬φ1 ∧ ¬φ2) ↔ φ1 ⇔ φ2 φ1 ∨ φ2 ↔ φ2 ∨ φ1 commutativity of "∨" φ1 ∨ (φ2 ∨ φ3) ↔ (φ1 ∨ φ2) ∨ φ3 associativity of "∨" (φ1 ∨ φ2) ∨ φ3 ↔ φ1 ∨ (φ2 ∨ φ3) associativity of "∨" φ1 ⇒ φ2 ↔ ¬φ1 ∨ φ2 φ1 ⇔ ¬φ2 ↔ ¬(φ1 ⇔ φ2) φ1 ⇔ φ2 ↔ (φ1 ⇒ φ2) ∧ (φ2 ⇒ φ1) φ1 ⇔ φ2 ↔ (φ1 ∧ φ2) ∨ (¬φ1 ∧ ¬φ2) φ1 ⇔ φ2 ↔ φ2 ⇔ φ1 commutativity of "⇔" φ1 ⇔ (φ2 ⇔ φ3) ↔ (φ1 ⇔ φ2) ⇔ φ3 associativity of "⇔" (φ1 ⇔ φ2) ⇔ φ3 ↔ φ1 ⇔ (φ2 ⇔ φ3) associativity of "⇔" (∀ν)[¬φ] ↔ ¬(∃ν)φ Generalized DeMorgan's Law
a.k.a. ∀ and ∃ are inverses(∀ν1)(∀ν2)[φ] ↔ (∀ν2)(∀ν1)[φ] (∃ν)[¬φ] ↔ ¬(∀ν)φ Generalized DeMorgan's Law
a.k.a. ∀ and ∃ are inverses(∃ν1)(∃ν2)[φ] ↔ (∃ν2)(∃ν1)[φ] Here are examples of proofs using the deduction Rewrite:
Proof of the following formula:(P → R) ∨ (Q → R) ≡ (P ∧ Q) → R
(#) Theorem/Subgoals We start working with the formula being proved
as follows:(1) We'll work on transforming the left-hand side of formula (1)
to the right-hand side as follows:(2) ≡ by rewriting the form " φ1 → φ2"
to "¬φ1 ∨ φ2"(3) ≡ by rewriting the form " φ1 → φ2"
to "¬φ1 ∨ φ2"(4) ≡ by simplifying (5) ≡ by rewriting the form " (φ1 ∨ φ2) ∨ φ3"
to "φ1 ∨ (φ2 ∨ φ3)"(6) ≡ by rewriting the form " φ1 ∨ φ2"
to "φ2 ∨ φ1"(7) ≡ by rewriting the form " φ1 ∨ (φ2 ∨ φ3)"
to "(φ1 ∨ φ2) ∨ φ3"(8) ≡ by rewriting the form " ¬φ1 ∨ ¬φ2"
to "¬(φ1 ∧ φ2)"(9) ≡ by rewriting the form " ¬φ1 ∨ φ2"
to "φ1 → φ2"(10) And that satisfies the earlier goal (1); i.e. we have: (11) That concludes this part of the proof. Thus, the theorem that was given is true.