Page **4** of **9**

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

Posted: **Wed May 15, 2019 4:16 am**

by **Scott Mayers**

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.

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

Posted: **Wed May 15, 2019 4:26 am**

by **PeteOlcott**

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.

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

Posted: **Wed May 15, 2019 7:51 am**

by **PeteOlcott**

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.

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

Posted: **Wed May 15, 2019 7:53 am**

by **Univalence**

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.

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

Posted: **Wed May 15, 2019 9:10 am**

by **Arising_uk**

Univalence wrote:And now that I am back ...

Told you, this place is addictive.

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

Posted: **Wed May 15, 2019 10:48 am**

by **Univalence**

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...

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

Posted: **Wed May 15, 2019 1:25 pm**

by **Arising_uk**

Seemed.

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

Posted: **Wed May 15, 2019 5:11 pm**

by **PeteOlcott**

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.

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

Posted: **Wed May 15, 2019 5:13 pm**

by **PeteOlcott**

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.

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

Posted: **Wed May 15, 2019 5:15 pm**

by **PeteOlcott**

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

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

Posted: **Wed May 15, 2019 5:52 pm**

by **Univalence**

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...

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

Posted: **Wed May 15, 2019 6:00 pm**

by **PeteOlcott**

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.

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

Posted: **Wed May 15, 2019 6:22 pm**

by **Univalence**

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.

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

Posted: **Wed May 15, 2019 6:30 pm**

by **PeteOlcott**

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.

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

Posted: **Wed May 15, 2019 6:34 pm**

by **Univalence**

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