Complétude de la théorie des ensembles intuitionniste globale

Le système séquentiel LJ de logique intuitionniste de Gentzen possède deux symboles d'implication. L'un est le symbole logique → et l'autre est le symbole métalogique ⇒ dans les séquents. En considérant le système logique LJ comme un objet mathématique, nous comprenons que les symboles logiques ∧, ∨, →, ¬, ∀, ∃ sont des opérateurs sur les formules, et ⇒ est une relation. C'est-à-dire que φ ⇒ Ψ est une phrase métalogique qui est vraie ou fausse, en comprenant que notre métalogique est une logique classique. En d'autres termes, nous discutons du système logique LJ dans la théorie des ensembles classique ZFC, dans laquelle φ ⇒ Ψ est une phrase. L'objectif de cet article est de formuler une théorie des ensembles intuitionniste ainsi que sa métathéorie. Dans Takeuti et Titani 6, nous avons formulé une théorie des ensembles intuitionniste ainsi que sa métathéorie basée sur la logique intuitionniste. Dans cet article, nous postulons que la métathéorie est basée sur la logique classique. Soit Ω un cHa. Ω peut être un ensemble de valeurs de vérité d'un modèle de LJ. Alors les symboles logiques ∧, ∨, →, ¬, ∀ x , ∃ x sont interprétés comme des opérateurs sur Ω, et la phrase φ ⇒ Ψ est interprétée comme 1 (vrai) ou 0 (faux). Cela signifie que le symbole métalogique ⇒ peut également être exprimé comme un opérateur logique tel que φ ⇒ Ψ est interprété comme 1 ou 0.