Does anyone here actually understand formal proofs of mathematical logic?

 Posts: 2074
 Joined: Wed Jul 08, 2015 1:53 am
 Location: Saskatoon, SK, Canada
Re: Does anyone here actually understand formal proofs of mathematical logic?
I'm also asking a question in [url=viewtopic.php?f=12&t=26619&p=409385#p409385]Is There such a reality as nonX for every X[/quote] that you guys might be interested in. It may help in part depending on your goal here.

 Posts: 970
 Joined: Mon Jul 25, 2016 6:55 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
It is simply that when we specify sound deductive inference as formal proofs ofScott Mayers wrote: ↑Wed May 15, 2019 4:12 amThank 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?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 2728
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 Γ”...
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.
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.

 Posts: 970
 Joined: Mon Jul 25, 2016 6:55 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
I now have my whole system boiled down to these three sentences:Scott Mayers wrote: ↑Wed May 15, 2019 4:12 amThank 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?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 2728
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 Γ”...
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.
Complete and consistent and formal systems are entirely specified by (1) and (2)
(1) True(x) is defined to be formal proofs to theorem consequences.
(2) Axioms are stipulated to be finite strings having the semantic property of Boolean True.

 Posts: 492
 Joined: Sun May 12, 2019 6:28 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
This is rather peculiar.PeteOlcott wrote: ↑Wed May 15, 2019 3:30 am The otherwise meaningless finite string "bachelor" inherits its semantic meaning from its parent: Marital_Status Boolean.False.
You said you aren't going to be using types, but you speak of a formal system where Stringtypes inherit semantics from Booleantypes.
Furthermore, since it is trivial to infer one's marital status from the knowledge that they are a bachelor, it seems rather intuitive (to me) that this is also a valid inference rule in your system: bachelor:String ⇒ Marital_Status: Boolean.True
Which leaves you with a cyclical graph and some concerns about type safety in your system.
 Arising_uk
 Posts: 12314
 Joined: Wed Oct 17, 2007 2:31 am
Re: Does anyone here actually understand formal proofs of mathematical logic?
Told you, this place is addictive.Univalence wrote:And now that I am back ...

 Posts: 492
 Joined: Sun May 12, 2019 6:28 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
Disposable email addresses and unmemorable passwords seems like a workable strategy...Arising_uk wrote: ↑Wed May 15, 2019 9:10 amTold you, this place is addictive.Univalence wrote:And now that I am back ...
 Arising_uk
 Posts: 12314
 Joined: Wed Oct 17, 2007 2:31 am

 Posts: 970
 Joined: Mon Jul 25, 2016 6:55 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
Univalence wrote: ↑Wed May 15, 2019 7:53 amThis is rather peculiar.PeteOlcott wrote: ↑Wed May 15, 2019 3:30 am The otherwise meaningless finite string "bachelor" inherits its semantic meaning from its parent: Marital_Status Boolean.False.
You said you aren't going to be using types, but you speak of a formal system where Stringtypes inherit semantics from Booleantypes.
Furthermore, since it is trivial to infer one's marital status from the knowledge that they are a bachelor, it seems rather intuitive (to me) that this is also a valid inference rule in your system: bachelor:String ⇒ Marital_Status: Boolean.True
Which leaves you with a cyclical graph and some concerns about type safety in your system.

 Posts: 970
 Joined: Mon Jul 25, 2016 6:55 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
The is the second time that I took a long time carefully composing a post, and then submit simply erased it.PeteOlcott wrote: ↑Wed May 15, 2019 5:11 pmUnivalence wrote: ↑Wed May 15, 2019 7:53 amThis is rather peculiar.PeteOlcott wrote: ↑Wed May 15, 2019 3:30 am The otherwise meaningless finite string "bachelor" inherits its semantic meaning from its parent: Marital_Status Boolean.False.
You said you aren't going to be using types, but you speak of a formal system where Stringtypes inherit semantics from Booleantypes.
Furthermore, since it is trivial to infer one's marital status from the knowledge that they are a bachelor, it seems rather intuitive (to me) that this is also a valid inference rule in your system: bachelor:String ⇒ Marital_Status: Boolean.True
Which leaves you with a cyclical graph and some concerns about type safety in your system.

 Posts: 970
 Joined: Mon Jul 25, 2016 6:55 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
Knowledge ontologies are inheritance hierarchies represented in acyclic graphs.PeteOlcott wrote: ↑Wed May 15, 2019 5:11 pmUnivalence wrote: ↑Wed May 15, 2019 7:53 amThis is rather peculiar.PeteOlcott wrote: ↑Wed May 15, 2019 3:30 am The otherwise meaningless finite string "bachelor" inherits its semantic meaning from its parent: Marital_Status Boolean.False.
You said you aren't going to be using types, but you speak of a formal system where Stringtypes inherit semantics from Booleantypes.
Furthermore, since it is trivial to infer one's marital status from the knowledge that they are a bachelor, it seems rather intuitive (to me) that this is also a valid inference rule in your system: bachelor:String ⇒ Marital_Status: Boolean.True
Which leaves you with a cyclical graph and some concerns about type safety in your system.
If you put cycles in the graph you are doing it wrong. Quine was wrong please get over it.
I created Minimal Type Theory so I know that types are needed.
https://www.researchgate.net/publicatio ... y_YACC_BNF
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

 Posts: 492
 Joined: Sun May 12, 2019 6:28 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
I am not even going to take the discussion into your epistemic criteria for “wrongness”.PeteOlcott wrote: ↑Wed May 15, 2019 5:15 pmKnowledge ontologies are inheritance hierarchies represented in acyclic graphs.PeteOlcott wrote: ↑Wed May 15, 2019 5:11 pmUnivalence wrote: ↑Wed May 15, 2019 7:53 am
This is rather peculiar.
You said you aren't going to be using types, but you speak of a formal system where Stringtypes inherit semantics from Booleantypes.
Furthermore, since it is trivial to infer one's marital status from the knowledge that they are a bachelor, it seems rather intuitive (to me) that this is also a valid inference rule in your system: bachelor:String ⇒ Marital_Status: Boolean.True
Which leaves you with a cyclical graph and some concerns about type safety in your system.
If you put cycles in the graph you are doing it wrong. Quine was wrong please get over it.
I am simply going to hold you accountable to your own standards.
If your graph is cyclical then your ontology wrong.
I showed you where your ontology is cyclical.
Therefore you are wrong.
Not only am I able to infer one’s marital status from one’s bachelor status, I am also able to infer one’s gender if I know that they are a bachelor.
You fail to recognize that the definition of “bachelor” is gendered. That is at least two bits of information...

 Posts: 970
 Joined: Mon Jul 25, 2016 6:55 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
No you certainly did not.Univalence wrote: ↑Wed May 15, 2019 5:52 pmOk. Then you are doing it wrong.PeteOlcott wrote: ↑Wed May 15, 2019 5:15 pmKnowledge ontologies are inheritance hierarchies represented in acyclic graphs.
If you put cycles in the graph you are doing it wrong. Quine was wrong please get over it.
I created Minimal Type Theory so I know that types are needed.
https://www.researchgate.net/publicatio ... y_YACC_BNF
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
I showed you where your ontology is cyclical.
I showed how it is inherently an acyclic graph and you showed how someone could intentionally screw this up.
Bachelor remains a meaningless string until it obtains is semantic value from its parent class.
Quine was wrong get over it.

 Posts: 492
 Joined: Sun May 12, 2019 6:28 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
Ok.PeteOlcott wrote: ↑Wed May 15, 2019 6:00 pmNo you certainly did not.Univalence wrote: ↑Wed May 15, 2019 5:52 pmOk. Then you are doing it wrong.PeteOlcott wrote: ↑Wed May 15, 2019 5:15 pm
Knowledge ontologies are inheritance hierarchies represented in acyclic graphs.
If you put cycles in the graph you are doing it wrong. Quine was wrong please get over it.
I created Minimal Type Theory so I know that types are needed.
https://www.researchgate.net/publicatio ... y_YACC_BNF
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
I showed you where your ontology is cyclical.
I showed how it is inherently an acyclic graph and you showed how someone could intentionally screw this up.
Bachelor remains a meaningless string until it obtains is semantic value from its parent class.
Quine was wrong get over it.
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.
You are desperately trying to reinvent dependent types and don’t even realize it.

 Posts: 970
 Joined: Mon Jul 25, 2016 6:55 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
Marital_Status.Boolean.False ◁ BachelorUnivalence wrote: ↑Wed May 15, 2019 6:22 pmOk.PeteOlcott wrote: ↑Wed May 15, 2019 6:00 pmNo you certainly did not.Univalence wrote: ↑Wed May 15, 2019 5:52 pm
Ok. Then you are doing it wrong.
I showed you where your ontology is cyclical.
I showed how it is inherently an acyclic graph and you showed how someone could intentionally screw this up.
Bachelor remains a meaningless string until it obtains is semantic value from its parent class.
Quine was wrong get over it.
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.
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.

 Posts: 492
 Joined: Sun May 12, 2019 6:28 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
And we are down to axiom of choice again...PeteOlcott wrote: ↑Wed May 15, 2019 6:30 pmMarital_Status.Boolean.False ◁ BachelorUnivalence wrote: ↑Wed May 15, 2019 6:22 pmOk.PeteOlcott wrote: ↑Wed May 15, 2019 6:00 pm
No you certainly did not.
I showed how it is inherently an acyclic graph and you showed how someone could intentionally screw this up.
Bachelor remains a meaningless string until it obtains is semantic value from its parent class.
Quine was wrong get over it.
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.
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.
Why have you chosen that particular inference rule?
Why didn’t you choose an inference rule from Bachelor:Noun > MaritalStatus:Boolean.True, Male:Gender