Does anyone here actually understand formal proofs of mathematical logic?

What is the basis for reason? And mathematics?

Moderators: AMod, iMod

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

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

Post by PeteOlcott »

Univalence wrote: Tue May 14, 2019 4:22 pm
PeteOlcott wrote: Tue May 14, 2019 4:19 pm
Univalence wrote: Tue May 14, 2019 4:08 pm

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
It does not matter what Boolean is.

(1) Some expressions of language are defined to have the semantic value of HibGiblet.
(2) Valid deductive inference is HibGiblet preserving.
(3) Therefore valid deductive inference on the basis of HibGiblet expressions necessarily derives a HibGiblet expression.
Within any formal system defined on the basis of sound deductive inference there are no expressions that are not HibGiblet decidable.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

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

Post by Univalence »

PeteOlcott wrote: Tue May 14, 2019 4:39 pm It does not matter what Boolean is.
PeteOlcott wrote: Tue May 14, 2019 4:39 pm Within any formal system defined on the basis of sound deductive inference there are no expressions that are not HibGiblet decidable.
The above two statements are incompatible with Type theory/Proof theory.

A Boolean is a type.

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

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

Post by PeteOlcott »

Univalence wrote: Tue May 14, 2019 4:48 pm
PeteOlcott wrote: Tue May 14, 2019 4:39 pm It does not matter what Boolean is.
PeteOlcott wrote: Tue May 14, 2019 4:39 pm Within any formal system defined on the basis of sound deductive inference there are no expressions that are not HibGiblet decidable.
The above two statements are incompatible with Type theory/Proof theory.

A Boolean is a Type and Dependent-type theory is Type-preserving then this should spells out "Peter, you are wrong".

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.
My system is only the sound deductive inference model itself so disagreeing with me is disagreeing with logic.
My system works just fine without the existence or the concept of types.

You start out with HibGiblet and apply HibGiblet preserving operations then you necessarily end up with HibGiblet.

it is not really that hard. Are you in psychological denial? It really sounds like you are in psychological denial.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

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

Post by Univalence »

PeteOlcott wrote: Tue May 14, 2019 4:55 pm My system is only the sound deductive inference model itself so disagreeing with me is disagreeing with logic.
My system works just fine without the existence or the concept of types.

You start out with HibGiblet and apply HibGiblet preserving operations then you necessarily end up with HibGiblet.

it is not really that hard. Are you in psychological denial? It really sounds like you are in psychological denial.
You can take a horse to water but you can't make it drink.

Good bye.
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

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

Post by PeteOlcott »

Univalence wrote: Tue May 14, 2019 4:56 pm
PeteOlcott wrote: Tue May 14, 2019 4:55 pm My system is only the sound deductive inference model itself so disagreeing with me is disagreeing with logic.
My system works just fine without the existence or the concept of types.

You start out with HibGiblet and apply HibGiblet preserving operations then you necessarily end up with HibGiblet.

it is not really that hard. Are you in psychological denial? It really sounds like you are in psychological denial.
Good bye.
I can handle any rational arguments against what I am saying.
There is no rational counter-argument to an irrational argument.
Are you the guy that believes that 1=0?
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

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

Post by Univalence »

PeteOlcott wrote: Tue May 14, 2019 4:59 pm Are you the guy that believes that 1=0?
It depends on what types of mathematical objects you have in mind when you USE the symbols 1, 0 and =

https://ncatlab.org/nlab/show/identity+type
https://en.wikipedia.org/wiki/Zero_ring
https://www.youtube.com/watch?v=WfDcrN5_1wA
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

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

Post by PeteOlcott »

Univalence wrote: Tue May 14, 2019 5:01 pm
PeteOlcott wrote: Tue May 14, 2019 4:59 pm Are you the guy that believes that 1=0?
It depends on what you mean by 1, 0 and =

https://ncatlab.org/nlab/show/identity+type
https://en.wikipedia.org/wiki/Zero_ring
https://www.youtube.com/watch?v=WfDcrN5_1wA
I am only using "1" and "0" as a placeholder for their actual meanings. When my
ontology of the common set of all knowledge is complete I will give you the GUID
that I am referring to.

Globally Unique Identifier, no other concept in the universe would have the same GUID.

If I said "big blog" and stinky cheese" as their place holders without stipulating these
unconventional word-labels the communication process would fail because decoding
would lack an appropriate basis.

In the communication process when I am saying that:
"I am going to the store to buy a pizza"
we do not have to explicitly stipulate the meaning of every word.
All of the words have default meanings and these meanings are
implicitly specified unless and until they are explicitly superseded.

Thus it is known that 1=0 is false unless and until a formal system is provided
in advance stipulating otherwise.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

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

Post by Univalence »

PeteOlcott wrote: Tue May 14, 2019 5:16 pm I am only using "1" and "0" as a placeholder for their actual meanings. When my
ontology of the common set of all knowledge is complete I will give you the GUID
that I am referring to.

Globally Unique Identifier, no other concept in the universe would have the same GUID.

If I said "big blog" and stinky cheese" as their place holders without stipulating these
unconventional word-labels the communication process would fail because decoding
would lack an appropriate basis.

In the communication process when I am saying that:
"I am going to the store to buy a pizza"
we do not have to explicitly stipulate the meaning of every word.
All of the words have default meanings and these meanings are
implicitly specified unless and until they are explicitly superseded.

Thus it is known that 1=0 is false unless and until a formal system is provided
in advance stipulating otherwise.
OK. Good luck and all the best.
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

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

Post by PeteOlcott »

Univalence wrote: Tue May 14, 2019 5:26 pm
PeteOlcott wrote: Tue May 14, 2019 5:16 pm I am only using "1" and "0" as a placeholder for their actual meanings. When my
ontology of the common set of all knowledge is complete I will give you the GUID
that I am referring to.

Globally Unique Identifier, no other concept in the universe would have the same GUID.

If I said "big blog" and stinky cheese" as their place holders without stipulating these
unconventional word-labels the communication process would fail because decoding
would lack an appropriate basis.

In the communication process when I am saying that:
"I am going to the store to buy a pizza"
we do not have to explicitly stipulate the meaning of every word.
All of the words have default meanings and these meanings are
implicitly specified unless and until they are explicitly superseded.

Thus it is known that 1=0 is false unless and until a formal system is provided
in advance stipulating otherwise.
OK. Good luck and all the best.
I created Minimal Type Theory because I know that types are useful.
https://www.researchgate.net/publicatio ... y_YACC_BNF

When trying to understand the barest essence of sound deductive inference,
types add extraneous inessential complexity that distracts attention away from
this barest essence.

Only when 100% perfectly complete total understanding of the barest possible
essence is achieved can we add further elaboration that could include such things as types.

If we don't do it this way total understanding may never ever occur.
Only when we examine things at their barest possible essence can we
divide several different misconceptions that have been conflated together.

If we don't do this these conflated misconceptions remain forever indivisible
and thus never analyzable. What is a clear mistake of reasoning is forever
perceived as a disagreement of opinion.
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

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

Post by PeteOlcott »

Univalence wrote: Tue May 14, 2019 4:48 pm
PeteOlcott wrote: Tue May 14, 2019 4:39 pm It does not matter what Boolean is.
PeteOlcott wrote: Tue May 14, 2019 4:39 pm Within any formal system defined on the basis of sound deductive inference there are no expressions that are not HibGiblet decidable.
The above two statements are incompatible with Type theory/Proof theory.
If any system of inference is incompatible with sound deductive inference then that system of inference is necessarily incorrect.

There is nothing wrong with type theory operations performed on a type result in the same type.
Type transforming operations derive isomorphisms.

There may be tens of thousands of proof theories that are incompatible with sound deductive
inference each and every one of these would be necessarily incorrect.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

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

Post by Univalence »

PeteOlcott wrote: Tue May 14, 2019 5:58 pm Only when 100% perfectly complete total understanding of the barest possible
essence is achieved can we add further elaboration that could include such things as types.
Then I must absolutely insist that you make your arguments without Boolean, Integer, Identity or Equality types while you elucidate on the essence in question.
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

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

Post by PeteOlcott »

Univalence wrote: Tue May 14, 2019 7:48 pm
PeteOlcott wrote: Tue May 14, 2019 5:58 pm Only when 100% perfectly complete total understanding of the barest possible
essence is achieved can we add further elaboration that could include such things as types.
Then I must absolutely insist that you make your arguments without Boolean, Integer, Identity or Equality types while you elucidate on the essence in question.
We have one 8 ounce cup of water (True premises) that is poured into another empty 8 ounce cup
such that no water is lost (valid deduction) and end up with another 8 ounce cup of water (True conclusion).

It is just like the assignment operation in computer science: (let) X = Y;
We are merely moving the value of Y into the location of X.

Denying sound deductive inference is the same as denying the computer science
assignment operation.

When we (let) X = Y, it is impossible for X to not have the value of Y.
In this same way the conclusion of sound deduction is necessarily always true.
It is merely moving the value of the true premises into the conclusion.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

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

Post by Univalence »

PeteOlcott wrote: Tue May 14, 2019 9:18 pm We have one 8 ounce cup of water (True premises) that is poured into another empty 8 ounce cup
such that no water is lost (valid deduction) and end up with another 8 ounce cup of water (True conclusion).
Ludic fallacy

Ignores adhesive interaction between water and cup and hence, ignores non-zero volume of water residue in original cup.
Ignores verificationist perspective. How do you know that the destination container actually contains 8 ounces post-facto?
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

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

Post by Univalence »

PeteOlcott wrote: Tue May 14, 2019 9:18 pm It is just like the assignment operation in computer science: (let) X = Y;
We are merely moving the value of Y into the location of X.

Denying sound deductive inference is the same as denying the computer science
assignment operation.
Argument from ignorance. You fail to discern Pass by value from pass by reference

Your argument is better expressed in Linear logic because water is a finite resource.
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

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

Post by PeteOlcott »

Univalence wrote: Tue May 14, 2019 10:42 pm
PeteOlcott wrote: Tue May 14, 2019 9:18 pm It is just like the assignment operation in computer science: (let) X = Y;
We are merely moving the value of Y into the location of X.

Denying sound deductive inference is the same as denying the computer science
assignment operation.
Argument from ignorance. You fail to discern Pass by value from pass by reference

Your argument is better expressed in Linear logic because water is a finite resource.
All that I am saying is that whenever you transmit anything from one place to another place that (by definition) it actually gets to that other place.
Post Reply