Re: How a True(X) predicate can be defined for the set of analytic knowledge

On 4/5/25 11:10 PM, olcott wrote:

On 4/5/2025 5:19 PM, Richard Damon wrote:

On 4/5/25 4:58 PM, olcott wrote:

On 4/5/2025 2:20 AM, Mikko wrote:

On 2025-04-03 19:33:41 +0000, olcott said:
>

On 4/3/2025 2:09 AM, Mikko wrote:

On 2025-04-03 02:51:32 +0000, olcott said:
>

On 4/2/2025 8:56 PM, Richard Damon wrote:

On 4/2/25 9:30 PM, olcott wrote:

On 4/2/2025 5:05 PM, Richard Damon wrote:

On 4/2/25 11:59 AM, olcott wrote:

On 4/2/2025 4:20 AM, Mikko wrote:

On 2025-04-01 17:51:29 +0000, olcott said:
>

>
All we have to do is make a C program that does this
with pairs of finite strings then it becomes self-evidently
correct needing no proof.

>
There already are programs that check proofs. But you can make your own
if you think the logic used by the existing ones is not correct.
>
If the your logic system is sufficiently weak there may also be a way to
make a C program that can construct the proof or determine that there is
none.
>

>
When we define a system that cannot possibly be inconsistent
then a proof of consistency not needed.

>
But you can't do that unless you limit the system to only have a finite number of statements expressible in it, and thus it can't handle most real problems
>

>
A system entirely comprised of Basic Facts and Semantic logical entailment cannot possibly be inconsistent.
>

>
Sure it can.
>
The problem is you need to be very careful about what you allow as your "Basic Facts", and if you allow the system to create the concept of the Natural Numbers, you can't verify that you don't actually have a contradition in it.
>

>
It never has been that natural numbers have
ever actually had any inconsistency themselves
they are essentially nothing more than an ordered
set of finite strings of digits.

>
No, but any logic system that can support them

>
Can be defined in screwy that has undecidability
or not defined in this screwy way.

>
And you can't define it otherwise.
>

>
Yes it free to keeps its screwy definition just like
set theory until a superior alternative comes along,
then it may be renamed naive formal systems.
>
A consistent set of stipulated axioms combined with
semantic logical entailment as the only inference step
makes undecidability impossible.

>
If semantic logical entaillment is allowed as an inference rule
the system is not formal. In order to be formal the system must
define "proof" as any string that satiisfies the syntactic rules
that the system specifies for proofs.
>

>
This "baffled" Richard
https://en.wikipedia.org/wiki/Montague_grammar
https://plato.stanford.edu/entries/montague-semantics/
Semantics as rich as natural language fully formalized
syntactically.
>

>
WHich doesn't "baffle" me, but doesn't define the LOGIC that the system uses, a fact that seems to baffle you, because you just don't understand what logic actually is.
>
Also note, this grammer doesn't remove the ambiguity inherent in the meaning of the words used, and especially can't handle the cases where the speaker was intentionally being vague to form a word play that extends the meaning of the word.

 It provides a system such that the full expressiveness
of natural language can be formalized thus enabling
the only inference step that my formal system architecture
requires: semantic logical entailment.
 

Your problem is that "Semantic Logica; Entailment" is powerful enough to create the Natural Number system with enough of its properties to allow Godel's proof, and thus your system must be incomplete, and being incomplete, it can't have Truth Predicate.
Sorry, but you just don't understand what you are talking about.
Do you accept that the existance or non-existance of a number that satisfies some finite specification has a truth value. Goldbach Conjecture must be either True or False, as either there is or there is Not an even number (greater than 4) not expressible as the sum of two primes. (We might not know the answer, but the answer exists, and might be found)
Do you accept that for something to be a proof, we need to be able to verify the correctness of the proof in finte operations?
And thus we could write an algorithm for that procedure to verify the proof?
Do you agree that because such a proof is expressed as a finite string of symbols we can create a number that represents it, by suitably defining an encoding system.
And thus we could write an algorithm, that given that number verifies that the proof is valid.
Do you agree, that a statement that isn't true, can not be proven in a consistent system.
So, it is possible to create a program whose output is whether or not a given claimed "proof" actually proves a given statement.
And thus the question of if a number exists that the program will accept is a valid question (as said proggram either have or not have a number it will accept)
And thus the statement that no such number exists is a valid statement.
And thus it is reasonable that Godel could create the program that verifies if a number represents a proof of that statement.
And if such a program exists, it can't actually accept any number, as any number existing makes the statement false, but also represents a proof that makes the statement true.
And there can't be a proof of that statement, as any such proof would be convertable into a number which the program then MUST accept, since it is a valid proof, which makes the statement wrong.
Thus the statement must be true, but unprovable.