Does anyone here actually understand formal proofs of mathematical logic?

 Posts: 730
 Joined: Mon Jul 25, 2016 6:55 pm
Does anyone here actually understand formal proofs of mathematical logic?
http://liarparadox.org/Provable_Mendelson.pdf
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.
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.
Last edited by PeteOlcott on Wed May 15, 2019 10:23 pm, edited 5 times in total.

 Posts: 3517
 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
In the meantime you might ask the Frenchman who would probably be the next best option

 Posts: 730
 Joined: Mon Jul 25, 2016 6:55 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
Logik and I had a fundamental disagreement in that he believed that 1=0 and could not be convinced otherwise.surreptitious57 wrote: ↑Mon May 13, 2019 10:58 pmLogik 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
This made rational dialogue pertaining to the mathematical formalization of the nature of truth impossible.

 Posts: 1403
 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 qualified but have to ask why you are always linking to nonsecure 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!
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!

 Posts: 730
 Joined: Mon Jul 25, 2016 6:55 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
Try this: https://philpapers.org/archive/OLCDSF.pdfScott Mayers wrote: ↑Tue May 14, 2019 12:46 amI'm qualified but have to ask why you are always linking to nonsecure 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!
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).

 Posts: 492
 Joined: Sun May 12, 2019 6:28 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
https://letsencrypt.org/PeteOlcott wrote: ↑Mon May 13, 2019 10:23 pmI don't pay the $50 for the SSL certificate for my Wordpress site.

 Posts: 492
 Joined: Sun May 12, 2019 6:28 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
And now that I am back I can simply ask: What do you mean by "equals"?PeteOlcott wrote: ↑Mon May 13, 2019 11:40 pmLogik and I had a fundamental disagreement in that he believed that 1=0 and could not be convinced otherwise.
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 CurryHowardLembek correspondence (which is the grounding for prooftheory in Univalent mathematics) you fail to grasp why that is significant for all Identity types
From the above "1 = 0" is a proposition whose truthvalue 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 truthvalue of your proposition is undecidable.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”.
And it doesn't stop there:
Different kinds of equality
What your misunderstanding prevents you from recognizing is that "1 = 0" could be any one of the above (in)equalities.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.
You were further provided an example where 1 = 0. An example which you failed to acknowledge.
https://en.wikipedia.org/wiki/Zero_ring
So to answer your question directly. Yes  some of us understand formal mathematical proofs. The question is: do you?The zero ring is the unique ring in which the additive identity 0 and multiplicative identity 1 coincide
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.

 Posts: 1403
 Joined: Wed Jul 08, 2015 1:53 am
 Location: Saskatoon, SK, Canada
Re: Does anyone here actually understand formal proofs of mathematical logic?
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.PeteOlcott wrote: ↑Tue May 14, 2019 4:36 amTry this: https://philpapers.org/archive/OLCDSF.pdfScott Mayers wrote: ↑Tue May 14, 2019 12:46 amI'm qualified but have to ask why you are always linking to nonsecure 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!
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).
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.

 Posts: 730
 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 amThank 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.PeteOlcott wrote: ↑Tue May 14, 2019 4:36 amTry this: https://philpapers.org/archive/OLCDSF.pdfScott Mayers wrote: ↑Tue May 14, 2019 12:46 amI'm qualified but have to ask why you are always linking to nonsecure 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!
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).
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.
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 Γ”...

 Posts: 730
 Joined: Mon Jul 25, 2016 6:55 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
I don't have any gap in my understanding.Univalence wrote: ↑Tue May 14, 2019 7:32 amAnd now that I am back I can simply ask: What do you mean by "equals"?PeteOlcott wrote: ↑Mon May 13, 2019 11:40 pmLogik and I had a fundamental disagreement in that he believed that 1=0 and could not be convinced otherwise.
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 CurryHowardLembek correspondence (which is the grounding for prooftheory in Univalent mathematics) you fail to grasp why that is significant for all Identity typesFrom the above "1 = 0" is a proposition whose truthvalue 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 truthvalue of your proposition is undecidable.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”.
And it doesn't stop there:
Different kinds of equalityWhat your misunderstanding prevents you from recognizing is that "1 = 0" could be any one of the above (in)equalities.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.
You were further provided an example where 1 = 0. An example which you failed to acknowledge.
https://en.wikipedia.org/wiki/Zero_ringSo to answer your question directly. Yes  some of us understand formal mathematical proofs. The question is: do you?The zero ring is the unique ring in which the additive identity 0 and multiplicative identity 1 coincide
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 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.

 Posts: 492
 Joined: Sun May 12, 2019 6:28 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
I guess we will continue to disagree then.
I will leave this video here, should you decide to reevaluate your stance.
Proof Theory Foundations

 Posts: 730
 Joined: Mon Jul 25, 2016 6:55 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
If you disagree with me than you are disagreeing thatUnivalence wrote: ↑Tue May 14, 2019 3:31 pmI guess we will continue to disagree then.
I will leave this video here, should you decide to reevaluate your stance.
Proof Theory Foundations
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.

 Posts: 492
 Joined: Sun May 12, 2019 6:28 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
I am not willing to rehash your ignorance.PeteOlcott wrote: ↑Tue May 14, 2019 4:00 pmIf 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).
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.

 Posts: 730
 Joined: Mon Jul 25, 2016 6:55 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
I am speaking at the metamathematical level. You are not speaking at the metamathematical level.Univalence wrote: ↑Tue May 14, 2019 4:08 pmI am not willing to rehash your ignorance.PeteOlcott wrote: ↑Tue May 14, 2019 4:00 pmIf 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).
This makes what you are saying offtopic.
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.

 Posts: 492
 Joined: Sun May 12, 2019 6:28 pm
Re: Does anyone here actually understand formal proofs of mathematical logic?
What's a Boolean, Peter?PeteOlcott wrote: ↑Tue May 14, 2019 4:19 pmI am speaking at the metamathematical level. You are not speaking at the metamathematical level.Univalence wrote: ↑Tue May 14, 2019 4:08 pmI am not willing to rehash your ignorance.PeteOlcott wrote: ↑Tue May 14, 2019 4:00 pmIf 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).
This makes what you are saying offtopic.
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.
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/idrislang/Idrisdev ... e/Bool.idr
Who is online
Users browsing this forum: No registered users and 1 guest