Les logiques : notes en vrac

[…] complete in the sense that semantic truth implies provability […]

Gödel thus showed that PA is consistent iff HA is consistent. This kind of result led him to think that Hilbert’s program was doomed.

Gödel à ainsi démontré que la PA est cohérence ssi l’HA est cohérente. Ce genre de résultat l’a amené à se dire que le programme de Hilbert était anéanti.

What else can we do with MetaPRL? We can also formulate incompatible theories in logical frameworks. For example, in Nuprl, our theory of partial recursive functions using bar types is incompatible with classical mathematics whereas most of Nuprl is compatible. So MetaPRL can isolated those results, which are a constructive version of Scott’s domain theory, related to Edinburgh LCF.

Que pouvons nous faire encore, avec MetaPRL ? Nous pouvons aussi formuler des théories incompatibles dans des cadriciels logiques. Par exemple, dans Nuprl, notre des fonctions partielles récursives utilisant des types brutes, est incompatibles avec les mathématiques classiques, avec lesquelles Nuprl est cependant compatibles. MetaPRL peut donc isoler ces résultats, qui sont des versions constructive de la théorie des domaines, de Scott, lié à la LCF d’Édimbourg.

Je ne sais pas quel cas Hilbert faisait des caractéristiques de son système, comme la correction (soundness), […]

Formal axiomatic systems were the key to showing the consistency of mathematics according to Hilbert […]

Denying the validity of P v ¬P is a consequence of constructive semantics, not a definition of intuitionism or constructivity.

La non‑reconnaissance de la validité de P v ¬P est une conséquence de la sémantique constructiviste, ce n’est pas par définition de l’intuitionnisme ou du constructivisme.

Now it is the contention of the intuitionists (or the constructivists, I shall use these terms synonymously) […]

Axioms of lambda calculus

• α‑equivalence: change of bound variable name, e.g., λx.E = λ y.E[y/x]
• β‑equivalence: application of function to arguments, e.g., (λx.E)y = E[y/x]
• η‑equivalence: elimination of redundant lambda‑abstractions, e.g., if x is bound in E, λx.(Ex) = E

Axiomes du lambda‑calcul

• α‑équivalence : renommage de variable liée, ex. λx.E = λ y.E[y/x]
• β‑équivalence: application de fonction à des arguments, ex. (λx.E)y = E[y/x]
• η‑équivalence: élimination de lambda‑abstractions redondantes, ex. si x est liée dans E, λx.(Ex) = E

This topic originated at the turn of the century with Russell's attempt to resolve his paradox through his “vicious Circle Principle” that “no totality can contain members defined in terms of itself”.

Ce sujet a pris naissance au tournant du siècle avec la tentative de Russel de résoudre son paradoxe qui par son « principe du cercle vicieux » fait que « aucune totalité ne peut être constituée d’élément définis en termes d’elle‑même ».