Does anyone here actually understand formal proofs of mathematical logic?

What is the basis for reason? And mathematics?

Moderators: AMod, iMod

PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

Re: Does anyone here actually understand formal proofs of mathematical logic?

Post by PeteOlcott »

Univalence wrote: Wed May 15, 2019 10:51 pm
PeteOlcott wrote: Wed May 15, 2019 10:51 pm Like I said you are like a guy being slapped in the face that does not believe in faces or slapping
A
A → B
-------
∴ B

I won't believe it until you write a Prolog interpreter that does higher order logic.
You are going to have to define all your terms.

I am most interested in the semantics/implementation of →

I will settle for code in Coq, Agda or Idris.
I make a fully executable solution to the halting problem and then you deduce on
the basis of the contradiction that 1=0 and the principle of explosion that computers
don't exist and use this as your new excuse to reject what I say.
Last edited by PeteOlcott on Wed May 15, 2019 11:01 pm, edited 1 time in total.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

Re: Does anyone here actually understand formal proofs of mathematical logic?

Post by Univalence »

PeteOlcott wrote: Wed May 15, 2019 10:59 pm I make a fully executable solution to the halting problem and then you deduce on
the basis of the contradiction that 1=0 and the principle of explosion that computers
don't exist and use this as your new excuse to reject what I say.
Nothing of what you have written here is executable, Pete.

Please don't lie.

Talk is cheap. Write the code.

Here is a compiler: https://tryidris.herokuapp.com/compile
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

Re: Does anyone here actually understand formal proofs of mathematical logic?

Post by PeteOlcott »

Univalence wrote: Wed May 15, 2019 11:00 pm
PeteOlcott wrote: Wed May 15, 2019 10:59 pm I make a fully executable solution to the halting problem and then you deduce on
the basis of the contradiction that 1=0 and the principle of explosion that computers
don't exist and use this as your new excuse to reject what I say.
Nothing of what you have written here is executable, Pete.

Please don't lie.
None of Aristotle's syllogisms were executable either and yet they
still formed the basis of all logic thus unequivocally proving that
your standard is unreasonable.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

Re: Does anyone here actually understand formal proofs of mathematical logic?

Post by Univalence »

PeteOlcott wrote: Wed May 15, 2019 11:02 pm None of Aristotle's syllogisms were executable either and yet they
still formed the basis of all logic thus unequivocally proving that
your standard is unreasonable.
My standard is objective.

Either you can produce an algorithm (thus allowing anybody with a computer to study and validate your claims) or you can't.

If you solved the halting problem you would be instantly able to solve all of the Millenium Prize Problems.

That's $6 million waiting for you and you are giving me flack about my "unreasonable standards"?
Just write the damn code then smile all the way to the bank.
Last edited by Univalence on Wed May 15, 2019 11:13 pm, edited 1 time in total.
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

Re: Does anyone here actually understand formal proofs of mathematical logic?

Post by PeteOlcott »

Univalence wrote: Wed May 15, 2019 11:04 pm
PeteOlcott wrote: Wed May 15, 2019 11:02 pm None of Aristotle's syllogisms were executable either and yet they
still formed the basis of all logic thus unequivocally proving that
your standard is unreasonable.
My standard is objective.

Either you can produce an algorithm (thus allowing anybody with a computer to study and validate your claims) or you can't.
Or I simply reject your absurd request as the next step of a never ending a head game.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

Re: Does anyone here actually understand formal proofs of mathematical logic?

Post by Univalence »

PeteOlcott wrote: Wed May 15, 2019 11:13 pm Or I simply reject your absurd request as the next step of a never ending a head game.
:lol: :lol: :lol:

So you don't want the $6 million then?
You don't want to alter the course of history and humanity for the better?
You don't want to create a multi-generational legacy by publishing a ground-breaking scientific discovery?

You just want a pat on the back and recognition from some strangers on a Philosophy forum.

Cool.
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

Re: Does anyone here actually understand formal proofs of mathematical logic?

Post by PeteOlcott »

Univalence wrote: Wed May 15, 2019 11:14 pm
PeteOlcott wrote: Wed May 15, 2019 11:13 pm Or I simply reject your absurd request as the next step of a never ending a head game.
:lol: :lol: :lol:

So you don't want the $6 million then?
You don't want to alter the course of history and humanity for the better?
You don't want to create a multi-generational legacy by publishing a ground-breaking scientific discovery?

You just want a pat on the back and recognition from some strangers on a Philosophy forum.

Cool.
The Prolog inference engine already implements this for every level of logic that it can handle.
True is when a query returns: Yes.
False is when the negation of a query returns Yes.
Deductively unsound is when a query returns No.
And that is all, making Prolog is both complete and consistent.
Last edited by PeteOlcott on Wed May 15, 2019 11:33 pm, edited 1 time in total.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

Re: Does anyone here actually understand formal proofs of mathematical logic?

Post by Univalence »

PeteOlcott wrote: Wed May 15, 2019 11:29 pm The Prolog inference engine already implements this for every level of logic that it can handle.
True is when a query returns: Yes.
Deductively unsound is when a query returns No.
Prolog is Turing-complete and therefore subject to the halting problem.
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

Re: Does anyone here actually understand formal proofs of mathematical logic?

Post by PeteOlcott »

Univalence wrote: Wed May 15, 2019 11:30 pm
PeteOlcott wrote: Wed May 15, 2019 11:29 pm The Prolog inference engine already implements this for every level of logic that it can handle.
True is when a query returns: Yes.
Deductively unsound is when a query returns No.
Prolog is Turing-complete and therefore subject to the halting problem.
Because Prolog implements the sound deductive inference model Godel's Incompleteness
can not be shown by Prolog because Prolog IS COMPLETE.

https://plato.stanford.edu/entries/goed ... mpleteness
The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried
out, there are statements of the language of F which can neither be
proved nor disproved in F. (Raatikainen 2018)

In Prolog an expression is either provable from facts and rules or it does not exist,
thus in Prolog there is no G in F that is unprovable, its provably true or not in F.

The sound deductive inference model works the same way. Expressions are either
provably true or deductively unsound.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

Re: Does anyone here actually understand formal proofs of mathematical logic?

Post by Univalence »

PeteOlcott wrote: Wed May 15, 2019 11:46 pm Because Prolog implements the sound deductive inference model Godel's Incompleteness
can not be shown by Prolog because Prolog IS COMPLETE.
Ohhhhh. Now I see what's going on.

You are confusing Logical completeness with Turing completeness

Lol. Godel's incompleteness pertains strictly to the claim that there are true expressions which cannot be arrived at via axiomatic deduction.
PeteOlcott wrote: Wed May 15, 2019 11:46 pm In Prolog an expression is either provable from facts and rules or it does not exist,
thus in Prolog there is no G in F that is unprovable, its provably true or not in F
It is precisely because the expression is unprovably-true (for a certain, precise meaning of "provable"), yet NOT in F is why we say that F is incomplete!
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

Re: Does anyone here actually understand formal proofs of mathematical logic?

Post by PeteOlcott »

Univalence wrote: Thu May 16, 2019 12:02 am
PeteOlcott wrote: Wed May 15, 2019 11:46 pm Because Prolog implements the sound deductive inference model Godel's Incompleteness
can not be shown by Prolog because Prolog IS COMPLETE.
Ohhhhh. Now I see what's going on.

You are confusing Logical completeness with Turing completeness

Lol. Godel's incompleteness pertains strictly to the claim that there are true sentences which cannot be arrived at via axiomatic deduction.
Hell no. You tried to change the subject and I changed it back.

"Godel's incompleteness pertains strictly to the claim that there are true
sentences which cannot be arrived at via axiomatic deduction."

AND the Sound deductive inference model proves this is impossible.
In the Sound deductive inference model True is ONLY PROVABLE TRUE,
thus NOT PROVABLE IS NOT TRUE.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

Re: Does anyone here actually understand formal proofs of mathematical logic?

Post by Univalence »

PeteOlcott wrote: Thu May 16, 2019 12:07 am AND the Sound deductive inference model proves this is impossible.
In the Sound deductive inference model True is ONLY PROVABLE TRUE,
thus NOT PROVABLE IS NOT TRUE.
Which is why I told you (in the very first post) that you don't understand Proof theory and dependent types.

Truth is a higher notion than proof. That you have chosen to assign it a Boolean value is just your arbitrary choice.
Last edited by Univalence on Thu May 16, 2019 12:12 am, edited 1 time in total.
wtf
Posts: 1178
Joined: Tue Sep 08, 2015 11:36 pm

Re: Does anyone here actually understand formal proofs of mathematical logic?

Post by wtf »

PeteOlcott wrote: Thu May 16, 2019 12:07 am AND the Sound deductive inference model proves this is impossible.
In the Sound deductive inference model True is ONLY PROVABLE TRUE,
thus NOT PROVABLE IS NOT TRUE.
Hilbert's failed dream.

https://en.wikipedia.org/wiki/Hilbert%27s_program

Wir müssen wissen.
Wir werden wissen.
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

Re: Does anyone here actually understand formal proofs of mathematical logic?

Post by PeteOlcott »

Univalence wrote: Thu May 16, 2019 12:09 am
PeteOlcott wrote: Thu May 16, 2019 12:07 am AND the Sound deductive inference model proves this is impossible.
In the Sound deductive inference model True is ONLY PROVABLE TRUE,
thus NOT PROVABLE IS NOT TRUE.
Which is why I told you (in the very first post) that you don't understand Proof theory and dependent types.

Truth is a higher notion than proof. That you have chosen to assign it a Boolean value is just your arbitrary choice.
TRUTH IS ONLY A SET OF MUTUALLY INTERLOCKING SEMANTIC TAUTOLOGIES, THUS
MAKING PROVABILITY NO MORE THAN VERIFYING THE CONNECTION BETWEEN TAUTOLOGIES.
IF THERE IS NO PROVABILITY THEN THERE IS NO CONNECTION AND THUS NO TRUTH.

You can yammer on and on about convoluted nonsense yet the above has remained the
nature of truth since the beginning of time.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

Re: Does anyone here actually understand formal proofs of mathematical logic?

Post by Univalence »

PeteOlcott wrote: Thu May 16, 2019 12:50 am TRUTH IS ONLY A SET OF MUTUALLY INTERLOCKING SEMANTIC TAUTOLOGIES, THUS
MAKING PROVABILITY NO MORE THAN VERIFYING THE CONNECTION BETWEEN TAUTOLOGIES.
IF THERE IS NO PROVABILITY THEN THERE IS NO CONNECTION AND THUS NO TRUTH.

You can yammer on and on about convoluted nonsense yet the above has remained the
nature of truth since the beginning of time.
Try using a larger font perhaps? One that's in proportion to your ignorance.

If you are going to be verifying the connections between nodes in a graph, you really ought to figure out who put the edges there in the first place and why.

Intent is a tricky thing to formalise.
Post Reply