Proof of Modus Ponens

- Let (1):P, (2):if P then Q, (3): not Q.
- (2)|-
- not P
- (1)|- P
- end case

- Q
- (3)|- not Q
- end case

|- If (if P then Q) and (if Q then R) then (if P then R).

- Let (1):if P then Q, (2):if Q then R, (3): not (if P then R).
- (3)|- (4): P, (5): not R.
- (1)|- following
- Case not P
- (4)|- RAA.
- end case

- (1): P or Q
- (2): if P then R
- (3): if Q then R
- (1)|-
- Case (4): P
- (2)|-
- Case not P
- (4): RAA.
- end case

- Case R
- end case

- ()|-R
- end case

- Case (5) Q,
- (3)|-
- Case not Q
- (5): RAA.
- end case

- Case R
- end case

- ()|- R
- end case

- Case must cover all the possibilities (but can overlap).
- Given P or Q... Case P, Case Q, ...
- Given not(P and Q and ...)... Case not P, Case not Q, ...
- Given (if P then Q). Case not P, Case Q
- Given (P iff Q...) Case P and Q..., Case not P and not Q...
- Given not(P iff Q) Case not P and Q, Case P and not Q.
- For any formula P. Case P, Case not P.
- Given not for 1 x(F(x)). Case for no x(F(x)) , Case for 2.. x(F(x))

- Some formulas Have only a single possibility made of a set of simpler formula
- not(P or Q or ...). Add not P, and not Q, ...
- P and Q. Add P, Q, ...
- not(if P then Q). Add P, and not Q
- not(not P). Add P
- for all x:T(F(x)). Add F(e) (where e is any expression of type T)
- not for all x:T(F(x)). Add not F(v) (where v was a free variable and is now bound to type T)
- for some x:T(F(x)). Add F(v) (where v was a free variable and is now bound to type T)
- not for some x:T(F(x)). Add not F(e) (where e is any expression of type T)
- for 1 x:T(F(x)). Add F(v), and for all x:T(if F(x) then x=v) (where v was a free variable and is now bound to type T)

- Three ways to end
- All cases end with RAA. Conclude ()|-RAA
- All cases end with RAA or the same formula C. Conclude ()|-C.
- Cases end with RAA or one of a number of formula C[i]. Conclude ()|-C[1] or C[2] or ... C[n].

# Notes on MATHS Notation

Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints, and give them a name. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents.

For a complete listing of pages in this part of my site by topic see [ home.html ]

# Notes on the Underlying Logic of MATHS

The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.For a more rigorous description of the standard notations see

- STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
# Glossary

- above::reason="I'm too lazy to work out which of the above statements I need here", often the last 2 or three statements.
- given::reason="I've been told that...", used to describe a problem.
- given::variable="I'll be given a value or object like this...", used to describe a problem.
- goal::theorem="The result I'm trying to prove right now".
- goal::variable="The value or object I'm trying to find or construct".
- let::reason="For the sake of argument let...", intoduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
- hyp::reason="I assumed this in my last Let/Case/Po/...".
- QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
- QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitte the goal you were given.
- RAA::conclusion="Reducto Ad Absurdum".