PeteOlcott wrote: ↑Tue Aug 13, 2019 9:51 pm
It is always necessarily the case that any relation expressible between two finite string expressions
of a language are necessarily provable in this same language.

Surely you are aware that Type-checking is still undecidable in System-F (and higher order lambda calculus)?

When we strip off all of the extraneous complexity of formal systems
and end up with ONLY stipulated relations between finite strings that
specify true(x) and provable(x) concurrently then we can see that they
cannot possibly diverge and any proof to the contrary is based on the
confusion of this extraneous complexity.

PeteOlcott wrote: ↑Tue Aug 13, 2019 10:45 pm
When we strip off all of the extraneous complexity of formal systems
and end up with ONLY stipulated relations between finite strings that
specify true(x) and provable(x) concurrently then we can see that they
cannot possibly diverge and any proof to the contrary is based on the
confusion of this extraneous complexity.

Earlier on you insisted that a cat is a TYPE of animal.

So now your system is complex enough to have the notion of types, but simple enough to have no undecidable statements.

You can't have it both ways. If your system has types, type-checking becomes undecidable (System F).
If you have sorts (System U) sort-checking becomes undecidable.

PeteOlcott wrote: ↑Tue Aug 13, 2019 10:45 pm
When we strip off all of the extraneous complexity of formal systems
and end up with ONLY stipulated relations between finite strings that
specify true(x) and provable(x) concurrently then we can see that they
cannot possibly diverge and any proof to the contrary is based on the
confusion of this extraneous complexity.

Earlier on you insisted that a cat is a TYPE of animal.

So now your system is complex enough to have the notion of types, but simple enough to have no undecidable statements.

You can't have it both ways. If your system has types, type-checking becomes undecidable (System F).
If you have sorts (System U) sort-checking becomes undecidable.

And if you have a system, your system becomes undecidable as it localized one phenomenon and approximates another.

PeteOlcott wrote: ↑Tue Aug 13, 2019 10:45 pm
When we strip off all of the extraneous complexity of formal systems
and end up with ONLY stipulated relations between finite strings that
specify true(x) and provable(x) concurrently then we can see that they
cannot possibly diverge and any proof to the contrary is based on the
confusion of this extraneous complexity.

Earlier on you insisted that a cat is a TYPE of animal.

So now your system is complex enough to have the notion of types, but simple enough to have no undecidable statements.

You can't have it both ways. If your system has types, type-checking becomes undecidable (System F).
If you have sorts (System U) sort-checking becomes undecidable.

You can come up with any convoluted reasoning that you like to confuse
yourself into believing that undecidable sentences exist, none-the-less
it is self-evident that any formal system comprised entirely of stipulated
relations between finite strings always simultaneously defines True(x)
and Provable(x), thus for these systems it is self-evident that undecidability
is impossible.

The key missing aspect of the above is the proof that such systems can express
any conceptual knowledge that can be expressed.

PeteOlcott wrote: ↑Tue Aug 13, 2019 10:45 pm
When we strip off all of the extraneous complexity of formal systems
and end up with ONLY stipulated relations between finite strings that
specify true(x) and provable(x) concurrently then we can see that they
cannot possibly diverge and any proof to the contrary is based on the
confusion of this extraneous complexity.

Earlier on you insisted that a cat is a TYPE of animal.

So now your system is complex enough to have the notion of types, but simple enough to have no undecidable statements.

You can't have it both ways. If your system has types, type-checking becomes undecidable (System F).
If you have sorts (System U) sort-checking becomes undecidable.

And if you have a system, your system becomes undecidable as it localized one phenomenon and approximates another.

Try and make a very simple concrete example of this.

Skepdick wrote: ↑Tue Aug 13, 2019 10:49 pm
Earlier on you insisted that a cat is a TYPE of animal.

So now your system is complex enough to have the notion of types, but simple enough to have no undecidable statements.

You can't have it both ways. If your system has types, type-checking becomes undecidable (System F).
If you have sorts (System U) sort-checking becomes undecidable.

And if you have a system, your system becomes undecidable as it localized one phenomenon and approximates another.

Try and make a very simple concrete example of this.

Yes, basic counting. Anything can be quantified, thus we may observe how a phenomenon exists in time and space, but we never really know its qualities.

The reverse works for qualifying a phenomenon into categories. I may qualify a rose but it does not take into account all the other types of flowers. Or I may qualifies flowers, but it does not take into account other organisms. The same applies for organisms and minerals etc.

Thus we are left with a paradox in the act of measurement and if any unity or synthesis is to be observed we have to look at common denominators.

Eodnhoj7 wrote: ↑Tue Aug 13, 2019 11:46 pm
And if you have a system, your system becomes undecidable as it localized one phenomenon and approximates another.

Try and make a very simple concrete example of this.

Yes, basic counting. Anything can be quantified, thus we may observe how a phenomenon exists in time and space, but we never really know its qualities.

The reverse works for qualifying a phenomenon into categories. I may qualify a rose but it does not take into account all the other types of flowers. Or I may qualifies flowers, but it does not take into account other organisms. The same applies for organisms and minerals etc.

Thus we are left with a paradox in the act of measurement and if any unity or synthesis is to be observed we have to look at common denominators.

I would estimate that you are using the term paradox incorrectly.

https://en.wikipedia.org/wiki/Paradox
A paradox is a statement that, despite apparently valid reasoning from true premises, leads to an apparently-self-contradictory or logically unacceptable conclusion.

PeteOlcott wrote: ↑Wed Aug 14, 2019 1:27 am
You can come up with any convoluted reasoning that you like to confuse
yourself into believing that undecidable sentences exist, none-the-less
it is self-evident that any formal system comprised entirely of stipulated
relations between finite strings always simultaneously defines True(x)
and Provable(x), thus for these systems it is self-evident that undecidability
is impossible.

It's called Girard's paradox... you can come up with any delusions of grandeur to convince yourself that you have solved decidability, incompleteness and consistency... but you haven't.

PeteOlcott wrote: ↑Wed Aug 14, 2019 1:27 am
The key missing aspect of the above is the proof that such systems can express
any conceptual knowledge that can be expressed.

You mean any conceptual knowledge, except the one you are 'forbidding' me from expressing because it breaks your system?

PeteOlcott wrote: ↑Wed Aug 14, 2019 2:33 amhttps://en.wikipedia.org/wiki/Paradox
A paradox is a statement that, despite apparently valid reasoning from true premises, leads to an apparently-self-contradictory or logically unacceptable conclusion.

This is begging the question. What is a "logically unacceptable" conclusion? The language you are using seems prescriptive rather than descriptive.

I am sure you've heard the good ol' paradox of omnipotence: Can God create an object that God himself cannot move?
I shall paraphrase this in context of the expressive power of a formal system: Can we create a formal system so powerful that it can prove a contradiction?

Try and make a very simple concrete example of this.

Yes, basic counting. Anything can be quantified, thus we may observe how a phenomenon exists in time and space, but we never really know its qualities.

The reverse works for qualifying a phenomenon into categories. I may qualify a rose but it does not take into account all the other types of flowers. Or I may qualifies flowers, but it does not take into account other organisms. The same applies for organisms and minerals etc.

Thus we are left with a paradox in the act of measurement and if any unity or synthesis is to be observed we have to look at common denominators.

I would estimate that you are using the term paradox incorrectly.

https://en.wikipedia.org/wiki/Paradox
A paradox is a statement that, despite apparently valid reasoning from true premises, leads to an apparently-self-contradictory or logically unacceptable conclusion.

False, it is correct.

In quantifying a phenomenon, the quantifier can mean an infinite number of things. However the quantifer only exists if something can be counted. This requires a quality. Thus in becoming more precise in a quantity, we become less precise in a quality. In counting oranges we lose detail about the qualities of the orange.

The reverse occurs.

In becoming defined in one thing, you become undefined in another. Increasing analysis results in increasing obscurity.

Eodnhoj7 wrote: ↑Tue Aug 13, 2019 11:46 pm
And if you have a system, your system becomes undecidable as it localized one phenomenon and approximates another.

Try and make a very simple concrete example of this.

Yes, basic counting. Anything can be quantified, thus we may observe how a phenomenon exists in time and space, but we never really know its qualities.

The reverse works for qualifying a phenomenon into categories. I may qualify a rose but it does not take into account all the other types of flowers. Or I may qualifies flowers, but it does not take into account other organisms. The same applies for organisms and minerals etc.

Thus we are left with a paradox in the act of measurement and if any unity or synthesis is to be observed we have to look at common denominators.

That is not really paradoxical at all.

https://en.wikipedia.org/wiki/Paradox
A paradox is a statement that, despite apparently valid reasoning from true premises, leads to an apparently-self-contradictory or logically unacceptable conclusion.

PeteOlcott wrote: ↑Wed Aug 14, 2019 1:27 am
You can come up with any convoluted reasoning that you like to confuse
yourself into believing that undecidable sentences exist, none-the-less
it is self-evident that any formal system comprised entirely of stipulated
relations between finite strings always simultaneously defines True(x)
and Provable(x), thus for these systems it is self-evident that undecidability
is impossible.

It's called Girard's paradox... you can come up with any delusions of grandeur to convince yourself that you have solved decidability, incompleteness and consistency... but you haven't.

Girard's paradox is the type-theoretic analogue of Russell's paradox in set theory.
Maybe proving my point would require showing how to eliminate each paradox one at a time.

I can't get a good handle on exactly what Girard's paradox is, a concrete example of minimal complexity would help.
I solved Russell's paradox paradox long ago. No physical or conceptual thing totally contains itself

Copyright Pete Olcott 2017

The idea of a set being a member of itself is exactly the same as a tin can entirely containing itself because physical containment and abstract containment inherit from the same base concept of {containment}, thus cannot possibly fundamentally differ.

PeteOlcott wrote: ↑Wed Aug 14, 2019 1:27 am
The key missing aspect of the above is the proof that such systems can express
any conceptual knowledge that can be expressed.

You mean any conceptual knowledge, except the one you are 'forbidding' me from expressing because it breaks your system?

You can form any logical incoherence that you want. the high level abstract notion of
a formal system from which every other formal system inherits calls out all logical
incoherence.

PeteOlcott wrote: ↑Wed Aug 14, 2019 2:33 amhttps://en.wikipedia.org/wiki/Paradox
A paradox is a statement that, despite apparently valid reasoning from true premises, leads to an apparently-self-contradictory or logically unacceptable conclusion.

This is begging the question. What is a "logically unacceptable" conclusion? The language you are using seems prescriptive rather than descriptive.

I am sure you've heard the good ol' paradox of omnipotence: Can God create an object that God himself cannot move?
I shall paraphrase this in context of the expressive power of a formal system: Can we create a formal system so powerful that it can prove a contradiction?

If that is "logically unacceptable" to you then make a choice.

Consistency, completeness, arithmetic or power. You have to throw away one.

I've thrown away the Aristotelian conception of consistency.

Can God create a stone too heavy for himself to lift?
Is really only asking: Is it an analytical impossibility for God to give up some of his power?

The simplest measure of logical incoherence is contradiction.
Every self contradictory expression of language must be rejected as logically incoherent:
"This sentence is not true"
"This sentence is not provable".
Must both be rejected.

PeteOlcott wrote: ↑Wed Aug 14, 2019 5:36 pm
Girard's paradox is the type-theoretic analogue of Russell's paradox in set theory.
Maybe proving my point would require showing how to eliminate each paradox one at a time.

Yes, it is. Girad's paradox affects Type Theory. And your forml system is called Minimal TYPE theory. Is it not?

If you have resolved Girard's paradox you have necessarily given up something. That's the nature of trade-offs. There's no such thing as free lunch.

PeteOlcott wrote: ↑Wed Aug 14, 2019 5:36 pm
I can't get a good handle on exactly what Girard's paradox is, a concrete example of minimal complexity would help.
I solved Russell's paradox paradox long ago. No physical or conceptual thing totally contains itself