## Does anyone here actually understand formal proofs of mathematical logic?

What is the basis for reason? And mathematics?

Moderators: AMod, iMod

Scott Mayers
Posts: 1819
Joined: Wed Jul 08, 2015 1:53 am

### 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 non-X for every X[/quote] that you guys might be interested in. It may help in part depending on your goal here.
PeteOlcott
Posts: 970
Joined: Mon Jul 25, 2016 6:55 pm

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

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.
PeteOlcott
Posts: 970
Joined: Mon Jul 25, 2016 6:55 pm

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

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.
I now have my whole system boiled down to these three sentences:
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.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

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

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.
This is rather peculiar.

You said you aren't going to be using types, but you speak of a formal system where String-types inherit semantics from Boolean-types.

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: 12313
Joined: Wed Oct 17, 2007 2:31 am

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

Univalence wrote:And now that I am back ...
Told you, this place is addictive.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

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

Arising_uk wrote: Wed May 15, 2019 9:10 am
Univalence wrote:And now that I am back ...
Told you, this place is addictive.
Disposable e-mail addresses and unmemorable passwords seems like a workable strategy...
Arising_uk
Posts: 12313
Joined: Wed Oct 17, 2007 2:31 am

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

Seemed.
PeteOlcott
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 am
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.
This is rather peculiar.

You said you aren't going to be using types, but you speak of a formal system where String-types inherit semantics from Boolean-types.

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.
PeteOlcott
Posts: 970
Joined: Mon Jul 25, 2016 6:55 pm

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

PeteOlcott wrote: Wed May 15, 2019 5:11 pm
Univalence wrote: Wed May 15, 2019 7:53 am
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.
This is rather peculiar.

You said you aren't going to be using types, but you speak of a formal system where String-types inherit semantics from Boolean-types.

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.
The is the second time that I took a long time carefully composing a post, and then submit simply erased it.
PeteOlcott
Posts: 970
Joined: Mon Jul 25, 2016 6:55 pm

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

PeteOlcott wrote: Wed May 15, 2019 5:11 pm
Univalence wrote: Wed May 15, 2019 7:53 am
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.
This is rather peculiar.

You said you aren't going to be using types, but you speak of a formal system where String-types inherit semantics from Boolean-types.

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.
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
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

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

PeteOlcott wrote: Wed May 15, 2019 5:15 pm
PeteOlcott wrote: Wed May 15, 2019 5:11 pm
Univalence 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 String-types inherit semantics from Boolean-types.

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.
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 am not even going to take the discussion into your epistemic criteria for “wrongness”.

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...
PeteOlcott
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 5:52 pm
PeteOlcott wrote: Wed May 15, 2019 5:15 pm
PeteOlcott wrote: Wed May 15, 2019 5:11 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
Ok. Then you are doing it wrong.

I showed you where your ontology is cyclical.
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.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

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

PeteOlcott wrote: Wed May 15, 2019 6:00 pm
Univalence wrote: Wed May 15, 2019 5:52 pm
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
Ok. Then you are doing it wrong.

I showed you where your ontology is cyclical.
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.
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.

You are desperately trying to reinvent dependent types and don’t even realize it.
PeteOlcott
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 6:22 pm
PeteOlcott wrote: Wed May 15, 2019 6:00 pm
Univalence wrote: Wed May 15, 2019 5:52 pm
Ok. Then you are doing it wrong.

I showed you where your ontology is cyclical.
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.
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.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

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

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