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: Thu May 16, 2019 3:14 am
PeteOlcott wrote: Thu May 16, 2019 3:11 am Not at all I do it with a conventional TM. I merely noticed a key detail that no one ever noticed before. I used a system of categorically exhaustively complete reasoning that is able to totally eliminate gaps in reasoning.
I think I have tolerated you long enough. I am happy to categorise you as a troll now.

And on the infinitesimal probability that I am wrong and you are right - spend your $6 million wisely.
You still can't understand that finding a different execution trace for the HP
would not fit into any of those categories?

This is going to blow my credibility with you even more, and I really don't care
credibility is a fake measure of truth.

I am saying this to you now because I keep forgetting the word ironic, so
I want to write it down somewhere where I can look it up later.

Wouldn't it be {Ironic} if I won the Turing prize for refuting Turing?

He would still be the father of computer science, yet like Einstein's
"God does not place dice with the universe"
would have been proven to have had a major blunder.
Scott Mayers
Posts: 2446
Joined: Wed Jul 08, 2015 1:53 am

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

Post by Scott Mayers »

PeteOlcott wrote: Wed May 15, 2019 9:44 pm
Introduction to Mathematical logic Sixth edition Elliott Mendelson (2015)
1.4 An Axiom System for the Propositional Calculus page 27-28
A wf C is said to be a consequence in S of a set Γ of wfs if and only if there is a
sequence B1, …, Bk of wfs such that C is Bk and, for each i, either Bi is an axiom
or Bi is in Γ, or Bi is a direct consequence by some rule of inference of some of
the preceding wfs in the sequence. Such a sequence is called a proof (or deduction)
of C from Γ. The members of Γ are called the hypotheses or premisses of the proof.
We use Γ ⊢ C as an abbreviation for “C is a consequence of Γ”...

I only have to use these links to avoid violating copyright law.
If you really do understand formal proofs of mathematical logic
then you don't need to go to these linked textbook pages.

It you can't understand what I mean by formal proof by the above paragraph alone
then you simply lack too much of the required prerequisite knowledge.
The textbook pages take someone all the way through the whole process
of learning everything about formal proofs of mathematical logic.
What you are showing above is ONLY about the proof of completeness and consistency of Propositional Calculus. It has no means of proving you know what you've read. What I complained about linking of you is that you are NOT arguing here but referencing YOUR work elsewhere rather than attempting to reconstruct it step by step here. Because every textbook on logic differs on how they express things, you require representing how YOU understand things in an appeal to the reader here, not by expecting us to do the work for you.

So you NEED to:

State a 'thesis' statement about your position when being 'formal'.

Define your terms and symbols here UNIQUELY.

Preface your proof's argument in colloquial language and express how you are going to go about proving/disproving your thesis.

...and I'm sure many others. But you have yet to clarify precisely what you are wanting to prove, what motivated your challenge, and why you think your perception of the prior theorems is appropriate.
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 »

Scott Mayers wrote: Sat May 18, 2019 4:51 pm
PeteOlcott wrote: Wed May 15, 2019 9:44 pm
Introduction to Mathematical logic Sixth edition Elliott Mendelson (2015)
1.4 An Axiom System for the Propositional Calculus page 27-28
A wf C is said to be a consequence in S of a set Γ of wfs if and only if there is a
sequence B1, …, Bk of wfs such that C is Bk and, for each i, either Bi is an axiom
or Bi is in Γ, or Bi is a direct consequence by some rule of inference of some of
the preceding wfs in the sequence. Such a sequence is called a proof (or deduction)
of C from Γ. The members of Γ are called the hypotheses or premisses of the proof.
We use Γ ⊢ C as an abbreviation for “C is a consequence of Γ”...

I only have to use these links to avoid violating copyright law.
If you really do understand formal proofs of mathematical logic
then you don't need to go to these linked textbook pages.

It you can't understand what I mean by formal proof by the above paragraph alone
then you simply lack too much of the required prerequisite knowledge.
The textbook pages take someone all the way through the whole process
of learning everything about formal proofs of mathematical logic.
What you are showing above is ONLY about the proof of completeness and consistency of Propositional Calculus. It has no means of proving you know what you've read. What I complained about linking of you is that you are NOT arguing here but referencing YOUR work elsewhere rather than attempting to reconstruct it step by step here. Because every textbook on logic differs on how they express things, you require representing how YOU understand things in an appeal to the reader here, not by expecting us to do the work for you.

So you NEED to:

State a 'thesis' statement about your position when being 'formal'.

Define your terms and symbols here UNIQUELY.

Preface your proof's argument in colloquial language and express how you are going to go about proving/disproving your thesis.

...and I'm sure many others. But you have yet to clarify precisely what you are wanting to prove, what motivated your challenge, and why you think your perception of the prior theorems is appropriate.
This single stipulated set of constraints transforms any formal system of any
level of logic into a complete and consistent formal system without any
undecidable sentences.

If the notion of True(x) is defined as provable from axioms and axioms are
stipulated to be finite strings having the semantic property of Boolean true
then every expression of language that not a theorem or an axiom is not true.

Here is what one reviewer on another forum said last night:
I agree with you that if your definitions are accepted then we can eliminate incompleteness.

I had to goad him into carefully studying and testing my specification before he would say
this. Prior to this he kept dismissing my words out-of-hand as ridiculous without even
bothering to read them.
Eodnhoj7
Posts: 8595
Joined: Mon Mar 13, 2017 3:18 am

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

Post by Eodnhoj7 »

PeteOlcott wrote: Mon May 13, 2019 11:40 pm
surreptitious57 wrote: Mon May 13, 2019 10:58 pm Logik has recently left us but if he ever returns then he would be the one to ask about this
In the meantime you might ask the Frenchman who would probably be the next best option
Logik and I had a fundamental disagreement in that he believed that 1=0 and could not be convinced otherwise.
This made rational dialogue pertaining to the mathematical formalization of the nature of truth impossible.
One does equal zero, just Google proofs for it.
Skepdick
Posts: 14364
Joined: Fri Jun 14, 2019 11:16 am

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

Post by Skepdick »

Eodnhoj7 wrote: Sun Aug 18, 2019 6:08 pm One does equal zero, just Google proofs for it.
All the proofs of 1=0 I've ever seen depend on some hidden division by zero. I think we can reasonably agree that dividing something by nothing is a meaningless notion.

The easier way to explode Mathematics is via infinity. https://en.wikipedia.org/wiki/Hilbert%2 ... rand_Hotel
What is the answer to ∞ - ∞ ? Intuitively it should be 0, right? If all the guests of an infinite hotel check out how many guests remain?

Then it follows:
∞ + 0 = ∞ + 1
(∞ + 0) - ∞ = (∞ + 1) - ∞
1 = 0

It is for this reason why ∞ - ∞ has been decreed "undefined". Otherwise Mathematics scores an own goal.
Eodnhoj7
Posts: 8595
Joined: Mon Mar 13, 2017 3:18 am

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

Post by Eodnhoj7 »

Skepdick wrote: Sun Aug 18, 2019 6:37 pm
Eodnhoj7 wrote: Sun Aug 18, 2019 6:08 pm One does equal zero, just Google proofs for it.
All the proofs of 1=0 I've ever seen depend on some hidden division by zero. I think we can reasonably agree that dividing something by nothing is a meaningless notion.


Not really, 0 is an individuator. The basic line is composed of infinite lines because it quite literally is divided by zero. Void canceling itself out would always result in an infinite number considering 0 is an undefined state.


The easier way to explode Mathematics is via infinity. https://en.wikipedia.org/wiki/Hilbert%2 ... rand_Hotel
What is the answer to ∞ - ∞ ? Intuitively it should be 0, right? If all the guests of an infinite hotel check out how many guests remain?

Then it follows:
∞ + 0 = ∞ + 1
(∞ + 0) - ∞ = (∞ + 1) - ∞
1 = 0

It is for this reason why ∞ - ∞ has been decreed "undefined". Otherwise Mathematics scores an own goal.
Skepdick
Posts: 14364
Joined: Fri Jun 14, 2019 11:16 am

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

Post by Skepdick »

Eodnhoj7 wrote: Sun Aug 18, 2019 9:07 pm
Not really, 0 is an individuator. The basic line is composed of infinite lines because it quite literally is divided by zero. Void canceling itself out would always result in an infinite number considering 0 is an undefined state.
Only proving my point.

From a contradiction anything follows.
Same goes for infinities.

Infinity is the principle of explosion in disguise.
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 »

Skepdick wrote: Sun Aug 18, 2019 9:10 pm Infinity is the principle of explosion in disguise.
What does that mean? You a Cantor denier?
Skepdick
Posts: 14364
Joined: Fri Jun 14, 2019 11:16 am

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

Post by Skepdick »

wtf wrote: Sun Aug 18, 2019 9:37 pm What does that mean? You a Cantor denier?
I mean that whereof one cannot speak, one must remain silent.
We can't do arithmetic with infinities without committing conceptual and symbolic equivocation.

∞ + 1 = ∞ (True)
∞ + 1 - ∞ = ∞ - ∞ (Undefined)
∞ + 2 = ∞ (True)
∞ + 1 > ∞ - 1 (False)

Wat?
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 »

Skepdick wrote: Sun Aug 18, 2019 9:41 pm
wtf wrote: Sun Aug 18, 2019 9:37 pm What does that mean? You a Cantor denier?
I mean that whereof one cannot speak, one must remain silent.
We can't speak of one infinity being greater than another infinity without committing conceptual and symbolic equivocation.

∞ + 1 = ∞ (True)
∞ + 1 - ∞ = ∞ - ∞ (Undefined)
∞ + 2 = ∞ (True)
∞ + 1 > ∞ - 1 (False)

Wat?
Are you unaware of transfinite set theory and the arithmetic of transfinite ordinals and cardinals? It's been a part of standard math since the 1870's.

I ask again. You deny the arithmetic of transfinite ordinals and cardinals? Ignorant of the subject or aware but a denier? Or arguing a finitist or ultrafinitist position?

https://en.wikipedia.org/wiki/Transfinite_number

https://en.wikipedia.org/wiki/Georg_Cantor

https://en.wikipedia.org/wiki/Ordinal_number

https://en.wikipedia.org/wiki/Cardinal_number

The use of the ∞ is only for the extended real numbers, and it's just a notational shorthand that we could do without, at the expense of wordiness.

https://en.wikipedia.org/wiki/Extended_real_number_line
Last edited by wtf on Sun Aug 18, 2019 10:02 pm, edited 1 time in total.
Skepdick
Posts: 14364
Joined: Fri Jun 14, 2019 11:16 am

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

Post by Skepdick »

wtf wrote: Sun Aug 18, 2019 9:56 pm Are you unaware of transfinite set theory and the arithmetic of transfinite ordinals and cardinals? It's been a part of standard math since the 1870's.

I ask again. You deny the arithmetic of transfinite ordinals and cardinals? Ignorant of the subject or aware but a denier? Or arguing a finitist or ultrafinitist position?
Yes, I am aware of it. It's part of model theory. I am arguing ultrafinitism. As usual.
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 »

Skepdick wrote: Sun Aug 18, 2019 10:02 pm Yes, I am aware of it. It's part of model theory. I am arguing ultrafinitism. As usual.
Was not aware that's your usual viewpoint. I'm a big fan of the work of the late Ed Nelson, the most prominent serious ultrafinitist. But arguing against the use of the infinity symbol in the extended real numbers as a notational shorthand in calculus seems excessive even for an ultrafnitist. Your criticism is off the mark in that regard.

Also, transfinite ordinals and cardinals are part of set theory, not model theory. Another remark off the mark. Have you formally studied ultrafinitism and infinity or is this just a curmedgeonly stance? If the latter, you need to tighten up your argument since your point is wrong as stated.
Skepdick
Posts: 14364
Joined: Fri Jun 14, 2019 11:16 am

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

Post by Skepdick »

wtf wrote: Sun Aug 18, 2019 10:05 pm Was not aware that's your usual viewpoint. I'm a big fan of the work of the late Ed Nelson, the most prominent serious ultrafinitist.
I arrived at ultrafinitism via Knuth/computer science.
wtf wrote: Sun Aug 18, 2019 10:05 pm But arguing against the use of the infinity symbol in the extended real numbers as a notational shorthand in calculus seems excessive even for an ultrafnitist. Your criticism is off the mark in that regard.
My criticism is not in that regard. In the normal sense, I am performatively contradicting myself. I use infinities in calculus.
Heck - Big-O notation is impossible without infinity limits.

But asymptotic behaviour is one thing. Manipulating infinities is another.
wtf wrote: Sun Aug 18, 2019 10:05 pm Also, transfinite ordinals and cardinals are part of set theory, not model theory.
Well, I am not sure about the internal compartmentalisation of Mathematics, but my familiarity of infinite cardinals is from reading about the Lownhein–Skolem theorem at some point.
wtf wrote: Sun Aug 18, 2019 10:05 pm Another remark off the mark. Have you formally studied ultrafinitism and infinity or is this just a curmedgeonly stance?
I have formally studied computer science (and this is what I currently practice). Hence my ultrafinitist bias - because finite time/memory.
Skepdick
Posts: 14364
Joined: Fri Jun 14, 2019 11:16 am

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

Post by Skepdick »

wtf wrote: Sun Aug 18, 2019 9:56 pm The use of the ∞ is only for the extended real numbers, and it's just a notational shorthand that we could do without, at the expense of wordiness.

https://en.wikipedia.org/wiki/Extended_real_number_line
In principle - all of this is true.

You can devise any alphabet/notation/functions and as all Mathematics goes - it will be internally consistent with the axioms that you have chosen (can it be any other way?)

In practice - it's an island. You can't integrate it into a single, coherent system with all other Mathematical knowledge because the behaviour of "=" becomes polymorphic around infinities and it does not play well with abstractions. I don't like compartmentalising my brain.
screwy.png
screwy.png (13.62 KiB) Viewed 2646 times
Eodnhoj7
Posts: 8595
Joined: Mon Mar 13, 2017 3:18 am

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

Post by Eodnhoj7 »

Skepdick wrote: Sun Aug 18, 2019 10:42 pm
wtf wrote: Sun Aug 18, 2019 9:56 pm The use of the ∞ is only for the extended real numbers, and it's just a notational shorthand that we could do without, at the expense of wordiness.

https://en.wikipedia.org/wiki/Extended_real_number_line
In principle - all of this is true.

You can devise any alphabet/notation/functions and as all Mathematics goes - it will be internally consistent with the axioms that you have chosen (can it be any other way?)

In practice - it's an island. You can't integrate it into a single, coherent system with all other Mathematical knowledge because the behaviour of "=" becomes polymorphic around infinities and it does not play well with abstractions. I don't like compartmentalising my brain.

screwy.png
Equality leads to contradiction thread.

Or something similar in name...old thread, can't remember the name.
Post Reply