On 4/22/2026 6:06 PM, André G. Isaak wrote:The point I want to make is that clarity and formalism are two different things. You do not excel at formalism. But that doesn't mean that you cannot be clear. Just worry about the English for the time being and worry about the formalism later.On 2026-04-22 01:48, olcott wrote:That certainly is more clear.On 4/22/2026 2:19 AM, Mikko wrote:>>It is a syntax error to use open variables φ in a definition.Besides>
KnownTrue is a bad name for a symbol that does not refer to knowledge.
>
KnownTrue :=
There exists a sequence of back-chained inference
steps Γ in PA such that φ reaches the axioms of PA
That doesn't solve the problem of the open variable.
>
You could solve this by changing it to KnownTrue(φ) := ...
>
But I still think your better off dispensing with the formalism and simply expressing your ideas in English since you always mangle the formalism.
>
Why not simply say:
>
A proposition is known to be true if there is a sequence of back-chained inference steps from that proposition to the axioms of Peano Arithmetic.
>
André
--
To email remove 'invalid' & replace 'gm' with well known Google mail service.
Les messages affichés proviennent d'usenet.