How to construct a formal proof?

What is the basis for reason? And mathematics?

Moderators: AMod, iMod

Post Reply
sadiadia
Posts: 1
Joined: Mon May 02, 2016 3:36 pm

How to construct a formal proof?

Post by sadiadia »

A ⊃ B, B ⊃ C, C ⊃ D /∴ A ⊃ ~(~C v ~D)

I've created the table in order to work through this, but I've no idea what steps to take to create a formal proof (using the proof method) to solve this.
Any help would be greatly appreciated.
User avatar
A_Seagull
Posts: 907
Joined: Thu Jun 05, 2014 11:09 pm

Re: How to construct a formal proof?

Post by A_Seagull »

To construct a formal proof, you first need a system, call it 'mathematics', 'logic' or 'whatever'.

Then you will need some axioms which will consist of the identification of some elements and some processes of inference.

You then take one or more of the elements and apply one or more of the processes of inference so that you arrive at something new; this is called a theorem. And you have just proved it. And it is true within the system that created it. And by recording each step of the process you will have created a formal proof. QED.
User avatar
NielsBohr
Posts: 219
Joined: Sat Aug 02, 2014 6:04 pm
Location: Switzerland
Contact:

Re: How to construct a formal proof?

Post by NielsBohr »

Poor times when science and letters are separated...

-Notice that the system "whatever" is the best; the one you create. Mathematics, as being in plural, are not a system. And logic is biased since Zeno. So you'll better have to create your own system.

-I guess you inserted the adjective "formal" to be accurate about "proof", but then, I'll ask you about "formal". As I as a site shows this (http://www.courvoisier-thevenaz.ch/logi ... sition.php), a demonstration (if you meant it) may absolutely not be a proof.

In few words, a demonstration stand only in its system, (and it is sufficient for this system not to be consistent, so that a disproof of this desmonstration occurs).

And even a proof may be re-taken back under questioning, as far as a proof is not the fact, but after the fact (so that artefacts may come into the account).

Depending on me, only the act in showing may constitute a "formal proof" - but this is very different from a demonstration. Such a proof should show in accordance with time, using most possible data in tis way. But demonstration absolutely may occur not to be temporal (as mainstream logic already is not temporal).

If you want deeper questions (and answers), see: http://milesmathis.com/.
Averroes
Posts: 535
Joined: Thu Jul 20, 2017 8:48 pm

Re: How to construct a formal proof?

Post by Averroes »

I am a “bit” late on this, but some people say, better late than never! If one can find some wisdom in that saying then here goes.

One thing to bear in mind in any logical and/or mathematical proofs, is that the first strategy to attempt to prove anything is the reductio ad absurdum. As the mathematician, G. H. Hardy said, "Reductio ad absurdum, which Euclid loved so much, is one of a mathematician's finest weapons. It is a far finer gambit than any chess gambit: a chess player may offer the sacrifice of a pawn or even a piece, but a mathematician offers the game" (Coxeter and Greitzer 1967, p. 16; Hardy 1993, p. 34)

So here too we make use of the Reductio to prove this.

For implication, I use the notation of the arrow pointing rightwards, instead of the “horseshoe”.

A→B, B→C, C→D, therefore A→ ~(~C v ~D)

..............(1) A→B...................Premise
..............(2) B→ C................. Premise
..............(3) C→D..................Premise
..............(4) A...................... Assumption (this assumption will be discarded with implication introduction rule)
..............(5) ~C v ~D.............. Assumption (assumption will be discarded with negation introduction rule)
..............(6) ~C.................... Assumption (assumption will be discarded with disjunction elimination rule)
.........1, 4(7) B.......................1, 4 →E (application of implication elimination rule)
.......1,2,4(8) C........................2,7 →E (implication elimination rule)
....1,2,4,6 (9) ꓕ (contradiction).....6,8 ~E (negation elimination rule)
............(10) ~D......................Assumption ( Will be discarded with disjunction elimination rule)
...1,2,3,4(11) D .......................3,8 →E
1,2,3,4,10(12) ꓕ (contradiction)....10, 11 ~E (application of negation elimination rule)
1,2,3,4,5 (13) ꓕ (contradiction).... 5,6,9,10,12 vE (application of disjunction elimination rule)
..1,2,3,4 (14) ~(~C v ~D).............13, 5 ~I (application of negation introduction rule)
....1,2,3 (15) A→ ~(~C v ~D).........4, 14 →I (application of implication introduction rule) □[/list]

From the systematic and strict application of the inference rules of sentential logic, the conclusion was proven to depend only on the premises. The numbers on the left hand side of the line numbers in the proof shows the assumptions and/or premises on which that line depends.

These kinds of proof require an ability to ‘see ahead’ of the particular application of a rule. So, in the exposition of the proof it is seen as systematic, but the route that leads to the proof is like stepping into the unknown armed only with the rules (and experience as well), so in that respect it cannot appropriately be said to be systematic; but is better described as creativity/artistic/ intuition/philosophical, but always within the perimeter set by the rules of thought, i.e. consistency.
ken
Posts: 2075
Joined: Mon May 09, 2016 4:14 am

Re: How to construct a formal proof?

Post by ken »

Averroes wrote: Sat Jul 22, 2017 7:43 am I am a “bit” late on this, but some people say, better late than never! If one can find some wisdom in that saying then here goes.

One thing to bear in mind in any logical and/or mathematical proofs, is that the first strategy to attempt to prove anything is the reductio ad absurdum. As the mathematician, G. H. Hardy said, "Reductio ad absurdum, which Euclid loved so much, is one of a mathematician's finest weapons. It is a far finer gambit than any chess gambit: a chess player may offer the sacrifice of a pawn or even a piece, but a mathematician offers the game" (Coxeter and Greitzer 1967, p. 16; Hardy 1993, p. 34)

So here too we make use of the Reductio to prove this.

For implication, I use the notation of the arrow pointing rightwards, instead of the “horseshoe”.

A→B, B→C, C→D, therefore A→ ~(~C v ~D)

..............(1) A→B...................Premise
..............(2) B→ C................. Premise
..............(3) C→D..................Premise
..............(4) A...................... Assumption (this assumption will be discarded with implication introduction rule)
..............(5) ~C v ~D.............. Assumption (assumption will be discarded with negation introduction rule)
..............(6) ~C.................... Assumption (assumption will be discarded with disjunction elimination rule)
.........1, 4(7) B.......................1, 4 →E (application of implication elimination rule)
.......1,2,4(8) C........................2,7 →E (implication elimination rule)
....1,2,4,6 (9) ꓕ (contradiction).....6,8 ~E (negation elimination rule)
............(10) ~D......................Assumption ( Will be discarded with disjunction elimination rule)
...1,2,3,4(11) D .......................3,8 →E
1,2,3,4,10(12) ꓕ (contradiction)....10, 11 ~E (application of negation elimination rule)
1,2,3,4,5 (13) ꓕ (contradiction).... 5,6,9,10,12 vE (application of disjunction elimination rule)
..1,2,3,4 (14) ~(~C v ~D).............13, 5 ~I (application of negation introduction rule)
....1,2,3 (15) A→ ~(~C v ~D).........4, 14 →I (application of implication introduction rule) □[/list]

From the systematic and strict application of the inference rules of sentential logic, the conclusion was proven to depend only on the premises. The numbers on the left hand side of the line numbers in the proof shows the assumptions and/or premises on which that line depends.

These kinds of proof require an ability to ‘see ahead’ of the particular application of a rule. So, in the exposition of the proof it is seen as systematic, but the route that leads to the proof is like stepping into the unknown armed only with the rules (and experience as well), so in that respect it cannot appropriately be said to be systematic; but is better described as creativity/artistic/ intuition/philosophical, but always within the perimeter set by the rules of thought, i.e. consistency.
WHY make an assumption in the first place?

Why not just look at what IS, already an actual fact?
Wyman
Posts: 974
Joined: Sat Jan 04, 2014 2:21 pm

Re: How to construct a formal proof?

Post by Wyman »

sadiadia wrote: Mon May 02, 2016 3:39 pm A ⊃ B, B ⊃ C, C ⊃ D /∴ A ⊃ ~(~C v ~D)

I've created the table in order to work through this, but I've no idea what steps to take to create a formal proof (using the proof method) to solve this.
Any help would be greatly appreciated.
A proof is like obscenity (according to a SC Justice) - you know it when you see it.

It depends on what your professor is requiring of you. Do you have axioms and rules of inference or are less formal proofs allowed?

If you are working with only modus ponens (including conditional proof):

Assume A (whatever follows from assuming A will create a conditional, If A then....)

Assuming A, by MP and the premises you stated, B follows

If B folllows, then C follows by MP and then D

So your conditional 'If A then ....' has given you B, C and D to work with.

From that, 'If A then C and D' follows directly by conditional proof

You now have to prove that 'C and D' is equivalent to not (not C or not D) and substitute it into the previous step to arrive at the conclusion.

I think you need more than modus ponens here, what do you think?

Perhaps do it this way: Assume the opposite and prove a contradiction (RAA)

Suppose (C and D) is equivalent to NOT(not (notC and notD))
Then we use the inference rule that says that double negatives cancel
This gives (C and D ) is equivalent to (notC and notD)
We then need the rule of separation (separating a conjunction into its component parts) applied several times, but it is fairly obvious already that (C and D) is contradictory to (notC and notD) - thus the conclusion is proven

So I did it with modus ponens, double negation and separation - can anyone do it with less rules of inference?
Averroes
Posts: 535
Joined: Thu Jul 20, 2017 8:48 pm

Re: How to construct a formal proof?

Post by Averroes »

Wyman wrote:It depends on what your professor is requiring of you. Do you have axioms and rules of inference or are less formal proofs allowed?

If you are working with only modus ponens (including conditional proof):

Assume A (whatever follows from assuming A will create a conditional, If A then....)

Assuming A, by MP and the premises you stated, B follows

If B folllows, then C follows by MP and then D

So your conditional 'If A then ....' has given you B, C and D to work with.

From that, 'If A then C and D' follows directly by conditional proof

You now have to prove that 'C and D' is equivalent to not (not C or not D) and substitute it into the previous step to arrive at the conclusion.

I think you need more than modus ponens here, what do you think?
That is a good strategy too, and as you rightly pointed out though, one would need more than MP in this strategy. One can show that (C & D) is equivalent to ~(~C v ~D) and as you will recall that is the famous DeMorgan Theorem. So that works too. So, with your strategy, it would look like this:
............(1) A→B...................Premise
............(2) B→ C................. Premise
............(3) C→D..................Premise
............(4) A...................... Assumption
.......1, 4(5) B.......................1, 4 →E (or MP)
.....1,2,4(6) C.......................2,5 →E (or MP)
...1,2,3,4(7) D ......................3,6 →E (or MP)
...1,2,3,4(8) C&D...................6,7 &I
..1,2,3,4 (9) ~(~C v ~D)........... 8 DeMorgan
..…1,2,3(10) A→ ~(~C v ~ D).....4, 9 →I □

But now to prove De Morgan, you have to make use of the disjunction elimination rule, as I did in my proof but without using DeMorgan. It looks like this:

DeMorgan Theorem states: C & D therefore ~(~C v ~D).

Proof:
.....(1) C & D.................Premise
.....(2) ~C v ~D..............Assumption
.....(3) ~C....................Assumption
...1(4) C......................1, &E
1,3 (5) ꓕ (contradiction)...3,4 ~E
.....(6) ~D....................Assumption
...1 (7) D.....................1, &E
1,6 (8) ꓕ (contradiction)...6,7 ~E
1,2 (9) ꓕ (contradiction)...2,3,5,6,8 vE
…1 (10) ~(~C v ~D)..........2, 9 ~I □

In this strategy, if there is a need to prove DeMorgan, you end up writing more lines! And thus it boils down to the same thing I wrote.
Wyman wrote:Suppose (C and D) is equivalent to NOT(not (notC and notD))
Then we use the inference rule that says that double negatives cancel
This gives (C and D ) is equivalent to (notC and notD)
We then need the rule of separation (separating a conjunction into its component parts) applied several times, but it is fairly obvious already that (C and D) is contradictory to (notC and notD) - thus the conclusion is proven
You mention assuming a semantic equivalence between (C&D) and ~(~(~C & ~D)) in an attempt to derive a contradiction, however, with that you cannot arrive at the conclusion because firstly they are not contradictory statements and secondly, in the conclusion to be proved there is a disjunction of negation, while in your assumption there is a conjunction of negation. But I think it was a typing mistake on your part which you then carried forward, as you had correctly mentioned a disjunction of negation before that line. So what you meant to assume to be equivalent (in a Reductio strategy I guess) was (C&D) and ~(~(~C v ~D)). But you could just as well have assumed (~C v ~D) and derive your contradiction before introducing a negation. In this way you would save yourself the step of having to apply a DN to get to the conclusion. And that is how DeMorgan was proved above.

As you mentioned equivalence, for completeness lets prove the other side as well, as an equivalence is a biconditional relation.

DeMorgan: ~(~C v ~D) therefore (C & D)

....(1) ~(~C v ~D)..............Premise
....(2) ~C........................Assumption
..2 (3) ~C v ~D..................2, vI (disjunction introduction)
1,2 (4) ꓕ (contradiction).... 1,3, ~E
..1 (5) ~~C .....................2, 4 ~I
..1 (6) C........................5 DN (Double Negation)
....(7) ~D......................Assumption
..7 (8) ~C v ~D ...............7, vI
1,7 (9) ꓕ (contradiction)....1, 8 ~E
1 (10) ~~D.....................7, 9 ~I
1 (11) D.......................10 DN
1 (12) C & D..................6, 11 &I □
Wyman wrote:can anyone do it with less rules of inference?
I do not think so. The way I did it is the strict minimum. Or else, one can consider writing the truth table, in which case there would be no need of any rules of inference at all!
Averroes
Posts: 535
Joined: Thu Jul 20, 2017 8:48 pm

Re: How to construct a formal proof?

Post by Averroes »

Ken wrote:WHY make an assumption in the first place?
Why not?

Ken wrote:Why not just look at what IS, already an actual fact?
And what would that be? 'The sky is blue on a sunny day', expresses a fact in the English language.

In formal logic, there is no such fact. In the problem in the OP, what would you consider as a fact? Is it the premises that you have in mind? But these are not facts. 'A→B' or 'B→C' or 'C→D' are not facts. These are merely a sequence of symbols which are given meaning by the syntax and semantics of formal logic which are expressed in the definitions of the particular system in use. In English, you have English grammar and the English dictionary which serve those purposes. But while in the English language, the proper nouns, the pronouns, the verbs, sentences etc… can refer to something in the real world; in logic the individual letters 'A', 'B' etc… do not refer. So, we did not start with a fact in the first place to which we could exclusively "look at". And that is exactly what we want in dealing with formal logic, i.e. abstraction from all content and attending merely to the form, hence its name 'formal logic'! In this way also, its use pervades all fields of study (mathematics, computer sciences, and philosophy par excellence, but also economics, legal studies and the humanities in general) because of this generality.

The importance of logic nowadays cannot be overestimated. As an example, take the DeMorgan Theorem (which was stated and proved in my previous post) which appears so simple and basic, but in fact it is of fundamental importance in the simplification of the design of the electronic circuits used in our computers. Simpler equivalent designs equates to better performance at reduced cost. Another example, take this philosophy forum itself, it is written in a computer language called PHP. To write/code just the registration and login system of this forum, tens if not a hundred of ‘if statements’ (i.e. conditionals) are required. And necessarily associated with each of these conditionals are the logical truth values TRUE or FALSE. In addition to that the conjunction, the disjunction and the negation are often found in those same conditionals

Concerning philosophy, logic is used to clarify and expose ambiguities in language, as often such ambiguities lead to fallacious arguments. In mathematics, the precision and economy of the statements expressed in the language of formal logic makes it indispensable. It does not even make sense to separate logic from mathematics, computer science and philosophy, as if these subjects could do without logic.

To conclude, without logic, there would be no philosophy for us to be having this conversation in the first place. Worse yet, there would not be the programming language in which this philosophy forum itself was written, hence no philosophy forum. Even worse, there would not even be computers on which the software package of this forum could be executed. And this is just concerning this small and casual discussion of ours. You can add to that the use of computers in the medical, engineering, financial and judicial field, and you get an idea of the importance of logic nowadays.
Wyman
Posts: 974
Joined: Sat Jan 04, 2014 2:21 pm

Re: How to construct a formal proof?

Post by Wyman »

Averroes wrote: Sun Jul 23, 2017 10:14 pm
Wyman wrote:It depends on what your professor is requiring of you. Do you have axioms and rules of inference or are less formal proofs allowed?

If you are working with only modus ponens (including conditional proof):

Assume A (whatever follows from assuming A will create a conditional, If A then....)

Assuming A, by MP and the premises you stated, B follows

If B folllows, then C follows by MP and then D

So your conditional 'If A then ....' has given you B, C and D to work with.

From that, 'If A then C and D' follows directly by conditional proof

You now have to prove that 'C and D' is equivalent to not (not C or not D) and substitute it into the previous step to arrive at the conclusion.

I think you need more than modus ponens here, what do you think?
That is a good strategy too, and as you rightly pointed out though, one would need more than MP in this strategy. One can show that (C & D) is equivalent to ~(~C v ~D) and as you will recall that is the famous DeMorgan Theorem. So that works too. So, with your strategy, it would look like this:
............(1) A→B...................Premise
............(2) B→ C................. Premise
............(3) C→D..................Premise
............(4) A...................... Assumption
.......1, 4(5) B.......................1, 4 →E (or MP)
.....1,2,4(6) C.......................2,5 →E (or MP)
...1,2,3,4(7) D ......................3,6 →E (or MP)
...1,2,3,4(8) C&D...................6,7 &I
..1,2,3,4 (9) ~(~C v ~D)........... 8 DeMorgan
..…1,2,3(10) A→ ~(~C v ~ D).....4, 9 →I □

But now to prove De Morgan, you have to make use of the disjunction elimination rule, as I did in my proof but without using DeMorgan. It looks like this:

DeMorgan Theorem states: C & D therefore ~(~C v ~D).

Proof:
.....(1) C & D.................Premise
.....(2) ~C v ~D..............Assumption
.....(3) ~C....................Assumption
...1(4) C......................1, &E
1,3 (5) ꓕ (contradiction)...3,4 ~E
.....(6) ~D....................Assumption
...1 (7) D.....................1, &E
1,6 (8) ꓕ (contradiction)...6,7 ~E
1,2 (9) ꓕ (contradiction)...2,3,5,6,8 vE
…1 (10) ~(~C v ~D)..........2, 9 ~I □

In this strategy, if there is a need to prove DeMorgan, you end up writing more lines! And thus it boils down to the same thing I wrote.
Wyman wrote:Suppose (C and D) is equivalent to NOT(not (notC and notD))
Then we use the inference rule that says that double negatives cancel
This gives (C and D ) is equivalent to (notC and notD)
We then need the rule of separation (separating a conjunction into its component parts) applied several times, but it is fairly obvious already that (C and D) is contradictory to (notC and notD) - thus the conclusion is proven
You mention assuming a semantic equivalence between (C&D) and ~(~(~C & ~D)) in an attempt to derive a contradiction, however, with that you cannot arrive at the conclusion because firstly they are not contradictory statements and secondly, in the conclusion to be proved there is a disjunction of negation, while in your assumption there is a conjunction of negation. But I think it was a typing mistake on your part which you then carried forward, as you had correctly mentioned a disjunction of negation before that line. So what you meant to assume to be equivalent (in a Reductio strategy I guess) was (C&D) and ~(~(~C v ~D)). But you could just as well have assumed (~C v ~D) and derive your contradiction before introducing a negation. In this way you would save yourself the step of having to apply a DN to get to the conclusion. And that is how DeMorgan was proved above.

As you mentioned equivalence, for completeness lets prove the other side as well, as an equivalence is a biconditional relation.

DeMorgan: ~(~C v ~D) therefore (C & D)

....(1) ~(~C v ~D)..............Premise
....(2) ~C........................Assumption
..2 (3) ~C v ~D..................2, vI (disjunction introduction)
1,2 (4) ꓕ (contradiction).... 1,3, ~E
..1 (5) ~~C .....................2, 4 ~I
..1 (6) C........................5 DN (Double Negation)
....(7) ~D......................Assumption
..7 (8) ~C v ~D ...............7, vI
1,7 (9) ꓕ (contradiction)....1, 8 ~E
1 (10) ~~D.....................7, 9 ~I
1 (11) D.......................10 DN
1 (12) C & D..................6, 11 &I □
Wyman wrote:can anyone do it with less rules of inference?
I do not think so. The way I did it is the strict minimum. Or else, one can consider writing the truth table, in which case there would be no need of any rules of inference at all!
Yes, the one snafu was a typo. But I tried to do it without DeMorgan's. I thought that (C & D) and (notC & notD) produced the contradiction for my RAA. For (C & D) reduces to C by separation and then (notC & not D) reduces to notC. So C & notC is the contradiction (the same with D and not D). Why is that not correct?
Averroes
Posts: 535
Joined: Thu Jul 20, 2017 8:48 pm

Re: How to construct a formal proof?

Post by Averroes »

Wyman wrote:Yes, the one snafu was a typo. But I tried to do it without DeMorgan's. I thought that (C & D) and (notC & notD) produced the contradiction for my RAA. For (C & D) reduces to C by separation and then (notC & not D) reduces to notC. So C & notC is the contradiction (the same with D and not D). Why is that not correct?
The problem is that if one tries to write the formal proof in this manner, one cannot prove the conclusion that way.

In a Reductio strategy, the purpose of showing a contradiction is to negate an assumption, and when one negates an assumption, the result of this negation does not depend on that assumption. However, in the way you describe, one does not assume what should have been assumed in the first place, and even if one ends up negating it, one does not prove what was required. This is how the "proof" looks like:

............(1) A→B...................Premise
............(2) B→ C................. Premise
............(3) C→D..................Premise
............(4) A...................... Assumption
.......1, 4(5) B.......................1, 4 →E (or MP)
.....1,2,4(6) C.......................2,5 →E (or MP)
...1,2,3,4(7) D ......................3,6 →E (or MP)
...1,2,3,4(8) C&D...................6,7 &I
............(9) ~C & ~ D.............Assumption
........9 (10) ~C.....................10, &E
1,2,4,9 (11) ꓕ(contradiction)....6, 9 ~E
...1,2,4 (12) ~(~C & ~ D)..........9, 11 ~I
....1,2 (13) A→~(~C & ~D).......4, 12 →I

With this sequence of steps, what was proved is this:

A→B, B→C therefore A→ ~(~C & ~D)

You will agree that this is not what was required.

The moral here is that if one takes the wrong turn, one cannot reach the destination. And also, if one has the wrong address one cannot arrive at the right place. Generally, this is bound to happen when we are attempting a proof because we make mistakes. But when we realize that this has happened, then we must consider taking a better way, until we arrive at the right place.

As you might recall, the history of mathematics and logic itself contains notorious mistakes by even the big names. But each time, the field got wiser by learning from these mistakes, and that re-oriented the various inquiries accordingly. And now you have the computer which drives our various machines.

Here is an interesting article I came across which captures some of these historical moments of mathematics and logic in an accessible language. If you would want to listen to the article instead, the audio version of the article is also available on the site:
https://www.theatlantic.com/technology/ ... er/518697/
Impenitent
Posts: 4330
Joined: Wed Feb 10, 2010 2:04 pm

Re: How to construct a formal proof?

Post by Impenitent »

constructing a formal proof...

tool-belts and tuxedos ...

unusual conjunction

-Imp
Post Reply