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

What is the basis for reason? And mathematics?

Moderators: AMod, iMod

PeteOlcott
Posts: 970
Joined: Mon Jul 25, 2016 6:55 pm

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

If you already understand formal proofs of mathematical logic you don't need
to look at the above textbook pages.

I don't pay the \$70 for the SSL certificate for my Wordpress site.

The above link totally explained the whole idea of formal proofs
I can't put all of that here without violating copyright law.

This is the key portion of the above PDF link.
Mendelson.png (139.37 KiB) Viewed 857 times
Last edited by PeteOlcott on Wed May 15, 2019 10:23 pm, edited 5 times in total.
surreptitious57
Posts: 4217
Joined: Fri Oct 25, 2013 6:09 am

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

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

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

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.
Scott Mayers
Posts: 1693
Joined: Wed Jul 08, 2015 1:53 am

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

I'm qualified but have to ask why you are always linking to non-secure sites? I can add the 's' for "https" but then get denied which tells me there is a concern about you linking to us here. It is even more concerning for people to open pdfs without sufficient trust rather than uploading images.

If you have any arguments, please turn your pdf into images and upload to present or take the effort to present it here. It takes a bit of effort to try to use the html but you CAN!
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: Tue May 14, 2019 12:46 am I'm qualified but have to ask why you are always linking to non-secure sites? I can add the 's' for "https" but then get denied which tells me there is a concern about you linking to us here. It is even more concerning for people to open pdfs without sufficient trust rather than uploading images.

If you have any arguments, please turn your pdf into images and upload to present or take the effort to present it here. It takes a bit of effort to try to use the html but you CAN!
Try this: https://philpapers.org/archive/OLCDSF.pdf

It loads directly in Google Chrome and quotes the key paragraph of the above link.
If you already know formal proofs of mathematical logic then you don't need to
look at the textbook pages.

A quick run down of the paper if you already totally understand both
[formal proofs of mathematical logic] and [sound deductive inference]:

I specify [Deductively sound formal proofs of mathematical logic]
based on [sound deductive inference]:
the conclusion of valid deductive inference necessarily follows from true premises.

I do this by simply stipulating that Axioms are true
(expressions of language defined to have the semantic value of Boolean True)

This stipulation by itself specifies this universal truth predicate: True(C) := (⊢ C).
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

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

PeteOlcott wrote: Mon May 13, 2019 10:23 pm I don't pay the \$50 for the SSL certificate for my Wordpress site.
https://letsencrypt.org/
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

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

PeteOlcott wrote: Mon May 13, 2019 11:40 pm Logik and I had a fundamental disagreement in that he believed that 1=0 and could not be convinced otherwise.
And now that I am back I can simply ask: What do you mean by "equals"?
I am not alone in asking this question: https://www.youtube.com/watch?v=WfDcrN5_1wA&t=42s

Firstly, because you fail to understand the implications of the Curry-Howard-Lembek correspondence (which is the grounding for proof-theory in Univalent mathematics) you fail to grasp why that is significant for all Identity types
In intensional type theory under the propositions as types paradigm, an identity type (or equality type) is the incarnation of equality. That is, for any type A and any terms x,y:A, the type IdA(x,y) is “the type of proofs that x=y” or “the type of reasons why x=y”.
From the above "1 = 0" is a proposition whose truth-value is yet to be proven and the reason you and I can't agree on it is because you have failed to state the types of your terms. What type of Mathematical objects are {0, 1} ? Until you state the types of your terms the truth-value of your proposition is undecidable.

And it doesn't stop there:

Different kinds of equality
Here is a list of distinctions between different notions of equality, in different contexts, where possibly all the following pairs of notions are, in turn, “the same”, just expressed in terms of different terminologies:

the difference between axiomatic and defined equality;
the difference between identity and equality,
the difference between intensional and extensional equality,
the difference between equality judgements and equality propositions,
the difference between equality and isomorphism,
the difference between equality and equivalence,
the possibility of operations that might not preserve equality.
What your misunderstanding prevents you from recognizing is that "1 = 0" could be any one of the above (in)equalities.
You were further provided an example where 1 = 0. An example which you failed to acknowledge.

https://en.wikipedia.org/wiki/Zero_ring
The zero ring is the unique ring in which the additive identity 0 and multiplicative identity 1 coincide
So to answer your question directly. Yes - some of us understand formal mathematical proofs. The question is: do you?

Apparently you come from a software background, so this video should help you close your gap in understanding, by explaining to you why none of the popular programming languages in use today actually support dependent types.
Scott Mayers
Posts: 1693
Joined: Wed Jul 08, 2015 1:53 am

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

PeteOlcott wrote: Tue May 14, 2019 4:36 am
Scott Mayers wrote: Tue May 14, 2019 12:46 am I'm qualified but have to ask why you are always linking to non-secure sites? I can add the 's' for "https" but then get denied which tells me there is a concern about you linking to us here. It is even more concerning for people to open pdfs without sufficient trust rather than uploading images.

If you have any arguments, please turn your pdf into images and upload to present or take the effort to present it here. It takes a bit of effort to try to use the html but you CAN!
Try this: https://philpapers.org/archive/OLCDSF.pdf

It loads directly in Google Chrome and quotes the key paragraph of the above link.
If you already know formal proofs of mathematical logic then you don't need to
look at the textbook pages.

A quick run down of the paper if you already totally understand both
[formal proofs of mathematical logic] and [sound deductive inference]:

I specify [Deductively sound formal proofs of mathematical logic]
based on [sound deductive inference]:
the conclusion of valid deductive inference necessarily follows from true premises.

I do this by simply stipulating that Axioms are true
(expressions of language defined to have the semantic value of Boolean True)

This stipulation by itself specifies this universal truth predicate: True(C) := (⊢ C).
Thank you. I don't mean to presume anything bad of you but we have to be cautious these days and the secure pages at least help. But we still need to know which particular means of expressing logic that you mean because there are many. If you can assert which source texts you may be using as a background you learned from, it might help prior to beginning or you might need to reproduce the background logic. My skill is originally from Lemmon's "Beginning Logic" for instance. I have discovered other authors that define their system with different symbols and means of expressing that are the same in essence but differ in HOW they approach this. I have a few sources but never all.

I've written an example proof before in some other thread of yours to which I'm not sure we share. I'll look it up later and link it to see if we share the same means of expressing. If not, we can try to match HOW we express things in common. That way, I or others can follow with this needs to be understood or we will have a hard time being sure we understand each other.

I'll get back to you later on this if you can tell us which sources you originally used for logic so that I could be fair in reading your proof properly.
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: Tue May 14, 2019 11:53 am
PeteOlcott wrote: Tue May 14, 2019 4:36 am
Scott Mayers wrote: Tue May 14, 2019 12:46 am I'm qualified but have to ask why you are always linking to non-secure sites? I can add the 's' for "https" but then get denied which tells me there is a concern about you linking to us here. It is even more concerning for people to open pdfs without sufficient trust rather than uploading images.

If you have any arguments, please turn your pdf into images and upload to present or take the effort to present it here. It takes a bit of effort to try to use the html but you CAN!
Try this: https://philpapers.org/archive/OLCDSF.pdf

It loads directly in Google Chrome and quotes the key paragraph of the above link.
If you already know formal proofs of mathematical logic then you don't need to
look at the textbook pages.

A quick run down of the paper if you already totally understand both
[formal proofs of mathematical logic] and [sound deductive inference]:

I specify [Deductively sound formal proofs of mathematical logic]
based on [sound deductive inference]:
the conclusion of valid deductive inference necessarily follows from true premises.

I do this by simply stipulating that Axioms are true
(expressions of language defined to have the semantic value of Boolean True)

This stipulation by itself specifies this universal truth predicate: True(C) := (⊢ C).
Thank you. I don't mean to presume anything bad of you but we have to be cautious these days and the secure pages at least help. But we still need to know which particular means of expressing logic that you mean because there are many. If you can assert which source texts you may be using as a background you learned from, it might help prior to beginning or you might need to reproduce the background logic. My skill is originally from Lemmon's "Beginning Logic" for instance. I have discovered other authors that define their system with different symbols and means of expressing that are the same in essence but differ in HOW they approach this. I have a few sources but never all.

I've written an example proof before in some other thread of yours to which I'm not sure we share. I'll look it up later and link it to see if we share the same means of expressing. If not, we can try to match HOW we express things in common. That way, I or others can follow with this needs to be understood or we will have a hard time being sure we understand each other.

I'll get back to you later on this if you can tell us which sources you originally used for logic so that I could be fair in reading your proof properly.

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

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

Univalence wrote: Tue May 14, 2019 7:32 am
PeteOlcott wrote: Mon May 13, 2019 11:40 pm Logik and I had a fundamental disagreement in that he believed that 1=0 and could not be convinced otherwise.
And now that I am back I can simply ask: What do you mean by "equals"?
I am not alone in asking this question: https://www.youtube.com/watch?v=WfDcrN5_1wA&t=42s

Firstly, because you fail to understand the implications of the Curry-Howard-Lembek correspondence (which is the grounding for proof-theory in Univalent mathematics) you fail to grasp why that is significant for all Identity types
In intensional type theory under the propositions as types paradigm, an identity type (or equality type) is the incarnation of equality. That is, for any type A and any terms x,y:A, the type IdA(x,y) is “the type of proofs that x=y” or “the type of reasons why x=y”.
From the above "1 = 0" is a proposition whose truth-value is yet to be proven and the reason you and I can't agree on it is because you have failed to state the types of your terms. What type of Mathematical objects are {0, 1} ? Until you state the types of your terms the truth-value of your proposition is undecidable.

And it doesn't stop there:

Different kinds of equality
Here is a list of distinctions between different notions of equality, in different contexts, where possibly all the following pairs of notions are, in turn, “the same”, just expressed in terms of different terminologies:

the difference between axiomatic and defined equality;
the difference between identity and equality,
the difference between intensional and extensional equality,
the difference between equality judgements and equality propositions,
the difference between equality and isomorphism,
the difference between equality and equivalence,
the possibility of operations that might not preserve equality.
What your misunderstanding prevents you from recognizing is that "1 = 0" could be any one of the above (in)equalities.
You were further provided an example where 1 = 0. An example which you failed to acknowledge.

https://en.wikipedia.org/wiki/Zero_ring
The zero ring is the unique ring in which the additive identity 0 and multiplicative identity 1 coincide
So to answer your question directly. Yes - some of us understand formal mathematical proofs. The question is: do you?

Apparently you come from a software background, so this video should help you close your gap in understanding, by explaining to you why none of the popular programming languages in use today actually support dependent types.
I don't have any gap in my understanding.
I am asking people to review a new type of formal system that I created
based on combining sound deductive inference with formal proofs of mathematical logic.
I wasn't having any success because people that didn't know mathematical logic were
trying to answer a mathematical logic questions.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

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

PeteOlcott wrote: Tue May 14, 2019 3:20 pm I don't have any gap in my understanding.
I guess we will continue to disagree then.

I will leave this video here, should you decide to re-evaluate your stance.

Proof Theory Foundations
PeteOlcott
Posts: 970
Joined: Mon Jul 25, 2016 6:55 pm

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

Univalence wrote: Tue May 14, 2019 3:31 pm
PeteOlcott wrote: Tue May 14, 2019 3:20 pm I don't have any gap in my understanding.
I guess we will continue to disagree then.

I will leave this video here, should you decide to re-evaluate your stance.

Proof Theory Foundations
If you disagree with me than you are disagreeing that
an expression of language derived from valid inference applied to true premises is necessarily true.

In other words disagreeing with me is disagreeing with sound deductive inference.
Anything outside the boundaries of [sound deductive inference] is off topic.

Truth is only:
(1) Expressions of language defined to have the semantic value of Boolean True.
(2) Valid deductions based on (1).

Induction only provides what appears to be an approximation of truth,
and (as the problem of induction proves) appearances can be deceiving.
Last edited by PeteOlcott on Tue May 14, 2019 4:08 pm, edited 1 time in total.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

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

PeteOlcott wrote: Tue May 14, 2019 4:00 pm If you disagree with me than you are disagreeing that
an expression of language derived from valid inference applied to true premises is necessarily true.

In other words disagreeing with me is disagreeing with sound deductive inference.
Anything outside the boundaries of [sound deductive inference] is off topic.

Truth is only:
(1) Expressions of language defined to have the semantic value of Boolean True.
(2) Valid deductions based on (1).
I am not willing to rehash your ignorance.

https://en.wikipedia.org/wiki/Dependent_type
Dependent types add complexity to a type system. Deciding the equality of dependent types in a program may require computations. If arbitrary values are allowed in dependent types, then deciding type equality may involve deciding whether two arbitrary programs produce the same result; hence type checking may become undecidable.
PeteOlcott
Posts: 970
Joined: Mon Jul 25, 2016 6:55 pm

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

Univalence wrote: Tue May 14, 2019 4:08 pm
PeteOlcott wrote: Tue May 14, 2019 4:00 pm If you disagree with me than you are disagreeing that
an expression of language derived from valid inference applied to true premises is necessarily true.

In other words disagreeing with me is disagreeing with sound deductive inference.
Anything outside the boundaries of [sound deductive inference] is off topic.

Truth is only:
(1) Expressions of language defined to have the semantic value of Boolean True.
(2) Valid deductions based on (1).
I am not willing to rehash your ignorance.
I am speaking at the meta-mathematical level. You are not speaking at the meta-mathematical level.
This makes what you are saying off-topic.

Truth is only:
(1) Expressions of language defined to have the semantic value of Boolean True.
(2) Valid deductions based on (1).

"Equality" could be stipulated to mean: {go get me an ice cream sandwich right now}
not even having any Boolean value.

The set of expressions of language defined to have the semantic value of Boolean true specifies
the basis of all inference within a formal system.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

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

PeteOlcott wrote: Tue May 14, 2019 4:19 pm
Univalence wrote: Tue May 14, 2019 4:08 pm
PeteOlcott wrote: Tue May 14, 2019 4:00 pm If you disagree with me than you are disagreeing that
an expression of language derived from valid inference applied to true premises is necessarily true.

In other words disagreeing with me is disagreeing with sound deductive inference.
Anything outside the boundaries of [sound deductive inference] is off topic.

Truth is only:
(1) Expressions of language defined to have the semantic value of Boolean True.
(2) Valid deductions based on (1).
I am not willing to rehash your ignorance.
I am speaking at the meta-mathematical level. You are not speaking at the meta-mathematical level.
This makes what you are saying off-topic.

Truth is only:
(1) Expressions of language defined to have the semantic value of Boolean True.
(2) Valid deductions based on (1).

"Equality" could be stipulated to mean: {go get me an ice cream sandwich right now}
not even having any Boolean value.

The set of expressions of language defined to have the semantic value of Boolean true specifies
the basis of all inference within a formal system.
What's a Boolean, Peter?

Somebody familiar with proof theory/dependent type systems would say that a Boolean is a Type.

Why, look! The developers of Idris agree with me.

https://github.com/idris-lang/Idris-dev ... e/Bool.idr