Does anyone here actually understand formal proofs of mathematical logic?

What is the basis for reason? And mathematics?

Moderators: AMod, iMod

Post Reply
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 6:34 pm
PeteOlcott wrote: Wed May 15, 2019 6:30 pm
Univalence wrote: Wed May 15, 2019 6:22 pm
Ok.

State your epistemic criteria for “rightness” and “wrongness”.

Nobody is “intentionally” screwing up the graph. You are intentionally pretending it is acyclic despite evidence to the contrary.
Marital_Status.Boolean.False ◁ Bachelor
The LHS is the parent the RHS is the child, the child points to its parent,
the parent does not point to its child, no cycles in the graph, Quine was wrong.
And we are down to axiom of choice again...

Why have you chosen that particular inference rule?

Why didn’t you choose an inference rule from Bachelor:Noun -> MaritalStatus:Boolean.True, Male:Gender
How are we down the axiom of choice?
How can this possibly make any difference?
The set of all general knowledge it finite.
Algorithmic compression is used to specify knowledge of infinite sets.

Things are the way that they are. Within general knowledge it is stipulated
that a dog is not a type of office building.

Likewise for martial status and bachelors. It could have been stipulated that
bachelors are anyone that likes to eat ice cream sandwiches, yet this was not stipulated.

I did not consider the term bachelorette as existing.
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 6:30 pm The LHS is the parent the RHS is the child, the child points to its parent,
You are going against the better judgment over the Composability over Inheritance principle...

https://en.wikipedia.org/wiki/Compositi ... e#Benefits
It is more natural to build business-domain classes out of various components than trying to find commonality between them and creating a family tree.
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 6:45 pm The set of all general knowledge it finite.
Sure. What is its cardinality and upper bound?

CARDINALITY(SET-ALL-KNOWLEDGE) > X : Boolean.False
CARDINALITY(SET-ALL-KNOWLEDGE) <= X : Boolean.True

Since you claim to have solved undecidability go ahead and determine X
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 6:47 pm
PeteOlcott wrote: Wed May 15, 2019 6:45 pm The set of all general knowledge it finite.
Sure. What is its cardinality and upper bound?

CARDINALITY(SET-ALL-KNOWLEDGE) > X : Boolean.False
CARDINALITY(SET-ALL-KNOWLEDGE) <= X : Boolean.True

Since you claim to have solved undecidability go ahead and determine X
Once you run out of general knowledge you have specified the finite set of all currently existing general knowledge.

Instead of going through these extraneous exercises why not try and understand how the following categorically proves my point.

Because valid deduction from true premises necessarily derives a true consequent we know that the following predicate pair consistently decides every deductively sound argument.

Introduction to Mathematical logic Sixth edition Elliott Mendelson (2015) Pages 27-28 http://liarparadox.org/Provable_Mendelson.pdf

The notion of complete and consistent formal systems is exhaustively elaborated as conventional formal proofs to theorem consequences where axioms are stipulated to be finite strings with the semantic property of Boolean true.
// LHS := RHS the LHS is defined as an alias for the RHS
∀x True(x) := ⊢x
∀x False(x) := ⊢¬x
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 6:59 pm Once you run out of general knowledge you have specified the finite set of all currently existing general knowledge.
You mean . once we stop learning.

When is that going to happen?
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 7:07 pm
PeteOlcott wrote: Wed May 15, 2019 6:59 pm Once you run out of general knowledge you have specified the finite set of all currently existing general knowledge.
You mean . once we stop learning.

When is that going to happen?
Once the system has every aspect of general knowledge up to the moment then it
continues to be updated as new general knowledge is created.

We have to place some kind of finite limit on the definition of the system to make
it feasible.
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 7:23 pm We have to place some kind of finite limit on the definition of the system to make
it feasible.
This is precisely the problem of choice.

Either solve this inequality or CHOOSE a value for X.

CARDINALITY(SET-ALL-KNOWLEDGE) > X : Boolean.False
CARDINALITY(SET-ALL-KNOWLEDGE) <= X : Boolean.True
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 7:37 pm
PeteOlcott wrote: Wed May 15, 2019 7:23 pm We have to place some kind of finite limit on the definition of the system to make
it feasible.
This is precisely the problem of choice.

Either solve this inequality or CHOOSE a value for X.

CARDINALITY(SET-ALL-KNOWLEDGE) > X : Boolean.False
CARDINALITY(SET-ALL-KNOWLEDGE) <= X : Boolean.True
I will do that as soon as you tell me the exact number of all of the birds in
the world, and you must prove that your count is correct.

I have no idea how many axioms specify the set of all general knowledge in
the same way that you have no idea exactly how many birds are in the world.
We don't need to know this. We only need to know that each is a finite set.
User avatar
Arising_uk
Posts: 12314
Joined: Wed Oct 17, 2007 2:31 am

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

Post by Arising_uk »

Pete wrote:
The is the second time that I took a long time carefully composing a post, and then submit simply erased it.
For some reason Pete the site is stopping browsers from caching pages so if you take a long time on your response the site times you out and when you hit submit you have to log back in and it just takes you back to the unedited quote and you can't hit back button to find a cached reply. The trick is to always copy your text before you hit the submit or preview just in case you've been logged out due to being, from the sites point of view, inactive. This way yoi can paste you reply back in. Hope this helps.
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 8:10 pm I will do that as soon as you tell me the exact number of all of the birds in
the world, and you must prove that your count is correct.

I have no idea how many axioms specify the set of all general knowledge in
the same way that you have no idea exactly how many birds are in the world.
We don't need to know this. We only need to know that each is a finite set.
Pete, you are going to be assigning GUIDs to your facts. At the very least you need to know if your GUIDs need to be 64, 128 or 256 bit integers.

It's your design. Why are you shifting all the responsibility for the uncertainty onto me?
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 4:26 am
Scott Mayers wrote: Wed May 15, 2019 4:12 am
PeteOlcott wrote: Tue May 14, 2019 3:11 pm http://liarparadox.org/Provable_Mendelson.pdf
Introduction to Mathematical logic Sixth edition Elliott Mendelson (2015) Page 27-28
Introduction to Mathematical logic Sixth edition Elliott Mendelson (2015) Page 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 Γ”...
Thank you. I'll have to look up this text to participate fairly. Were you still trying to disprove the Incompleteness theorems or is this something else?

This is a metalogic for proving some system closed closed on its domain and consistent among its axioms. It might be good to go step by step here to lay out what your ideal goal is (rather than 'lead' without others knowing what you are aiming for). I thought you intended to USE proofs within some system or other.
It is simply that when we specify sound deductive inference as formal proofs of
mathematical logic that Gödel incompleteness and Tarski undefinability cease to exist.

I have had this in the back of my mind for about 30 years and now finally have the
way to precisely specify it so that it can be verified as correct by anyone totally
understanding formal proofs of mathematical logic. It took me that long to translate
my intuitions into math.
Okay. I give up on you on this quest. It is like one asserting they can prove the Pythagorean Theorem as false. I'm not sure what you're expecting but while the theorem speaks of incompleteness, it is precisely only about limitations upon using a binary-only system of logic based on 'true/false' factors. I already agree that there are ways around any difficulties of the limitations. But the limitations in reality, apart from those incorrectly interpreting the theorems as making logic itself out to be faulty, are superficial with respect to the whole.
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 »

Arising_uk wrote: Wed May 15, 2019 8:23 pm
Pete wrote:
The is the second time that I took a long time carefully composing a post, and then submit simply erased it.
For some reason Pete the site is stopping browsers from caching pages so if you take a long time on your response the site times you out and when you hit submit you have to log back in and it just takes you back to the unedited quote and you can't hit back button to find a cached reply. The trick is to always copy your text before you hit the submit or preview just in case you've been logged out due to being, from the sites point of view, inactive. This way yoi can paste you reply back in. Hope this helps.
I am not logged out, it just erases my post and I am still logged in.
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: Wed May 15, 2019 8:45 pm
PeteOlcott wrote: Wed May 15, 2019 4:26 am
Scott Mayers wrote: Wed May 15, 2019 4:12 am
Thank you. I'll have to look up this text to participate fairly. Were you still trying to disprove the Incompleteness theorems or is this something else?

This is a metalogic for proving some system closed closed on its domain and consistent among its axioms. It might be good to go step by step here to lay out what your ideal goal is (rather than 'lead' without others knowing what you are aiming for). I thought you intended to USE proofs within some system or other.
It is simply that when we specify sound deductive inference as formal proofs of
mathematical logic that Gödel incompleteness and Tarski undefinability cease to exist.

I have had this in the back of my mind for about 30 years and now finally have the
way to precisely specify it so that it can be verified as correct by anyone totally
understanding formal proofs of mathematical logic. It took me that long to translate
my intuitions into math.
Okay. I give up on you on this quest. It is like one asserting they can prove the Pythagorean Theorem as false. I'm not sure what you're expecting but while the theorem speaks of incompleteness, it is precisely only about limitations upon using a binary-only system of logic based on 'true/false' factors. I already agree that there are ways around any difficulties of the limitations. But the limitations in reality, apart from those incorrectly interpreting the theorems as making logic itself out to be faulty, are superficial with respect to the whole.
You only have to take a few minutes and trace through this simple reasoning to confirm that I am obviously correct.

Introduction to Mathematical logic Sixth edition Elliott Mendelson (2015) Pages 27-28
http://liarparadox.org/Provable_Mendelson.pdf

The notion of complete and consistent formal systems is exhaustively elaborated as conventional formal proofs to theorem consequences where axioms are stipulated to be finite strings with the semantic property of Boolean true.

// LHS := RHS the LHS is defined as an alias for the RHS
∀x True(x) := ⊢x
∀x False(x) := ⊢¬x

Because valid deduction from true premises necessarily derives a true consequent we know that the above predicate pair consistently decides every deductively sound argument.
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:01 pm
Scott Mayers wrote: Wed May 15, 2019 8:45 pm
PeteOlcott wrote: Wed May 15, 2019 4:26 am

It is simply that when we specify sound deductive inference as formal proofs of
mathematical logic that Gödel incompleteness and Tarski undefinability cease to exist.

I have had this in the back of my mind for about 30 years and now finally have the
way to precisely specify it so that it can be verified as correct by anyone totally
understanding formal proofs of mathematical logic. It took me that long to translate
my intuitions into math.
Okay. I give up on you on this quest. It is like one asserting they can prove the Pythagorean Theorem as false. I'm not sure what you're expecting but while the theorem speaks of incompleteness, it is precisely only about limitations upon using a binary-only system of logic based on 'true/false' factors. I already agree that there are ways around any difficulties of the limitations. But the limitations in reality, apart from those incorrectly interpreting the theorems as making logic itself out to be faulty, are superficial with respect to the whole.
You only have to take a few minutes and trace through this simple reasoning to confirm that I am obviously correct.

Introduction to Mathematical logic Sixth edition Elliott Mendelson (2015) Pages 27-28
http://liarparadox.org/Provable_Mendelson.pdf

The notion of complete and consistent formal systems is exhaustively elaborated as conventional formal proofs to theorem consequences where axioms are stipulated to be finite strings with the semantic property of Boolean true.

// LHS := RHS the LHS is defined as an alias for the RHS
∀x True(x) := ⊢x
∀x False(x) := ⊢¬x

Because valid deduction from true premises necessarily derives a true consequent we know that the above predicate pair consistently decides every deductively sound argument.
You don't make sense here at all. I don't know if you are being real and it appears that you MAY be just playing people here. I notice that if you discover someone like myself use some logical argument elsewhere, you opt to select a more obscure one you hope the readers couldn't follow but make it seem that you know what you are talking about.

Let's see, YOU upturn Godel's intensely argued theorem in only a mere few minutes of reading? And though you fail constantly, you keep up the same tactic.


WARNING TO OTHERS: DO NOT USE THIS GUY'S LINKS. There is something wrong here and it CAN be a "honeypot" being used to DROP something on your computer! If this guy cannot argue here and ONLY here without an insistence on his links, there is something amiss. Pete, you keep begging you have powerful proof of something but cannot competently express this to me.....someone who DOES have a lot of background on this and STILL can't understand you.
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: Wed May 15, 2019 9:32 pm
PeteOlcott wrote: Wed May 15, 2019 9:01 pm
Scott Mayers wrote: Wed May 15, 2019 8:45 pm
Okay. I give up on you on this quest. It is like one asserting they can prove the Pythagorean Theorem as false. I'm not sure what you're expecting but while the theorem speaks of incompleteness, it is precisely only about limitations upon using a binary-only system of logic based on 'true/false' factors. I already agree that there are ways around any difficulties of the limitations. But the limitations in reality, apart from those incorrectly interpreting the theorems as making logic itself out to be faulty, are superficial with respect to the whole.
You only have to take a few minutes and trace through this simple reasoning to confirm that I am obviously correct.

Introduction to Mathematical logic Sixth edition Elliott Mendelson (2015) Pages 27-28
http://liarparadox.org/Provable_Mendelson.pdf

The notion of complete and consistent formal systems is exhaustively elaborated as conventional formal proofs to theorem consequences where axioms are stipulated to be finite strings with the semantic property of Boolean true.

// LHS := RHS the LHS is defined as an alias for the RHS
∀x True(x) := ⊢x
∀x False(x) := ⊢¬x

Because valid deduction from true premises necessarily derives a true consequent we know that the above predicate pair consistently decides every deductively sound argument.
You don't make sense here at all. I don't know if you are being real and it appears that you MAY be just playing people here. I notice that if you discover someone like myself use some logical argument elsewhere, you opt to select a more obscure one you hope the readers couldn't follow but make it seem that you know what you are talking about.

Let's see, YOU upturn Godel's intensely argued theorem in only a mere few minutes of reading? And though you fail constantly, you keep up the same tactic.


WARNING TO OTHERS: DO NOT USE THIS GUY'S LINKS. There is something wrong here and it CAN be a "honeypot" being used to DROP something on your computer! If this guy cannot argue here and ONLY here without an insistence on his links, there is something amiss. Pete, you keep begging you have powerful proof of something but cannot competently express this to me.....someone who DOES have a lot of background on this and STILL can't understand you.
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.
Last edited by PeteOlcott on Wed May 15, 2019 10:10 pm, edited 4 times in total.
Post Reply