Une TM qui stoppe ssi ZFC est inconsistant

foys a écrit:

militantisme mensonger

foys a écrit:

Ben voyons, c'est pourtant ce que fait COQ.

foys a écrit:

Prière d'insérer ci-dessous le programme qui fait ça avant de traiter tout le monde d'abruti. Je ne sais pas qui est ce find.

christophe c a écrit:

De toute façon, rassure-toi, aucun système formel n'est construit sur ces bases, on a découvert plus tard qu'une preuve de $\forall x R(x)$ est une preuve de $R(x)$

G.A. a écrit:

Elle s'est arrêtée ! Ah non pardon c'est mon ordi qui bug :-D

christophe c a écrit:

Mais je ne parle pas de preuve "méta" !!!!!!! angry smiley Je te parle de bonnes et dues preuves de chez preuves de chez le marchand de formel le plus acariatre grinning smiley . Je te parle du fait que dès lors que pour chaque n, tu as une preuve de chez preuve absolue de $R(n)$, tu as un programme qui à chaque $n$ t'associe une preuve de chez Super-preuve!

christophe c a écrit:

Par exemple $K$ peut recevoir à tel heure, pour telles raisons le commentaire $A \to (B \to A)$, mais ça n'en fera pas un $K$ tout nouveau tout beau qui a envie de sortir la nuit pour montrer ses nouveaux habits. Ca reste ton bon vieux $K$ bien familier tel que $\forall x,y: Kxy$qui est un commutateur langagier AVANT qu'on tente de l'enfermer dans une sémantique partielle où il y aurait "un $K$, en quelque sorte ,par $(A^B)^A$.

christophe c a écrit:

A la base, c'est très simple: une garantie de $\forall x R(x)$c'est un élément de l'intersection des ensembles $R(a)$ (j'amidonne un peu les notations) quand a parcourt l'univers.

C'est vraiment important. J'insiste bien que $\forall x R(x)$ est un ENSEMBLE qui est INCLUS DANS $R(a)$.

J'utilise bien le mot "garantie". (Du peu que je sais de COQ, il y aurait une option qui restitue cette garantie une fois entrée ta preuve, mais je connais trop peu ce logiciel, c'est juste une rumeur que j'ai entendue.)

Coq < Check plus_com.
plus_com
     : forall a b : nat, a + b = b + a

Coq < Print plus_com.
plus_com = 
fun a : nat =>
nat_ind (fun a0 : nat => forall b : nat, a0 + b = b + a0)
  (fun b : nat =>
   nat_ind (fun b0 : nat => 0 + b0 = b0 + 0) eq_refl
     (fun (b0 : nat) (IHb : 0 + b0 = b0 + 0) =>
      eq_ind (0 + b0) (fun n : nat => S b0 = S n) eq_refl (b0 + 0) IHb) b)
  (fun (a0 : nat) (IHa : forall b : nat, a0 + b = b + a0) (b : nat) =>
   eq_ind_r (fun n : nat => S n = b + S a0)
     (eq_ind (S (b + a0)) (fun n : nat => S (b + a0) = n) eq_refl 
        (b + S a0) (plus_n_Sm b a0)) (IHa b)) a
     : forall a b : nat, a + b = b + a

Argument scopes are [nat_scope nat_scope]

Coq < Compute plus_com.
     = fun a : nat =>
       (fix Ffix (x : nat) :
          forall x0 : nat,
          (fix Ffix0 (x1 x2 : nat) {struct x1} : nat :=
             match x1 with
             | 0 => x2
             | S x3 => S (Ffix0 x3 x2)
             end) x x0 =
          (fix Ffix0 (x1 x2 : nat) {struct x1} : nat :=
             match x1 with
             | 0 => x2
             | S x3 => S (Ffix0 x3 x2)
             end) x0 x :=
          match
            x as c
            return
              (forall x0 : nat,
               (fix Ffix0 (x1 x2 : nat) {struct x1} : nat :=
                  match x1 with
                  | 0 => x2
                  | S x3 => S (Ffix0 x3 x2)
                  end) c x0 =
               (fix Ffix0 (x1 x2 : nat) {struct x1} : nat :=
                  match x1 with
                  | 0 => x2
                  | S x3 => S (Ffix0 x3 x2)
                  end) x0 c)
          with
          | 0 =>
              fun x0 : nat =>
              (fix Ffix0 (x1 : nat) :
                 x1 =
                 (fix Ffix1 (x2 x3 : nat) {struct x2} : nat :=
                    match x2 with
                    | 0 => x3
                    | S x4 => S (Ffix1 x4 x3)
                    end) x1 0 :=
                 match
                   x1 as c
                   return
                     (c =
                      (fix Ffix1 (x2 x3 : nat) {struct x2} : nat :=
                         match x2 with
                         | 0 => x3
                         | S x4 => S (Ffix1 x4 x3)
                         end) c 0)
                 with
                 | 0 => eq_refl
                 | S x2 =>
                     match Ffix0 x2 in (_ = x3) return (S x2 = S x3) with
                     | eq_refl => eq_refl
                     end
                 end) x0
          | S x0 =>
              fun x1 : nat =>
              match
                match
                  Ffix x0 x1 in (_ = x2)
                  return
                    (x2 =
                     (fix Ffix0 (x3 x4 : nat) {struct x3} : nat :=
                        match x3 with
                        | 0 => x4
                        | S x5 => S (Ffix0 x5 x4)
                        end) x0 x1)
                with
                | eq_refl => eq_refl
                end in (_ = x2)
                return
                  (S x2 =
                   (fix Ffix0 (x3 x4 : nat) {struct x3} : nat :=
                      match x3 with
                      | 0 => x4
                      | S x5 => S (Ffix0 x5 x4)
                      end) x1 (S x0))
              with
              | eq_refl =>
                  match
                    plus_n_Sm x1 x0 in (_ = x2)
                    return
                      (S
                         ((fix Ffix0 (x3 x4 : nat) {struct x3} : nat :=
                             match x3 with
                             | 0 => x4
                             | S x5 => S (Ffix0 x5 x4)
                             end) x1 x0) = x2)
                  with
                  | eq_refl => eq_refl
                  end
              end
          end) a
     : forall a b : nat, a + b = b + a

Coq < Check (plus_com 1).
plus_com 1
     : forall b : nat, 1 + b = b + 1

Coq < Check (plus_com 0).
plus_com 0
     : forall b : nat, 0 + b = b + 0

Coq < Check (plus_com 1 2).
plus_com 1 2
     : 1 + 2 = 2 + 1

Coq < Compute (plus_com 0).  
     = fun b : nat =>
       (fix Ffix (x : nat) :
          x =
          (fix Ffix0 (x0 x1 : nat) {struct x0} : nat :=
             match x0 with
             | 0 => x1
             | S x2 => S (Ffix0 x2 x1)
             end) x 0 :=
          match
            x as c
            return
              (c =
               (fix Ffix0 (x0 x1 : nat) {struct x0} : nat :=
                  match x0 with
                  | 0 => x1
                  | S x2 => S (Ffix0 x2 x1)
                  end) c 0)
          with
          | 0 => eq_refl
          | S x0 =>
              match Ffix x0 in (_ = x1) return (S x0 = S x1) with
              | eq_refl => eq_refl
              end
          end) b
     : forall b : nat, 0 + b = b + 0

Coq < Compute (plus_com 1).
     = fun b : nat =>
       match
         match
           (fix Ffix (x : nat) :
              x =
              (fix Ffix0 (x0 x1 : nat) {struct x0} : nat :=
                 match x0 with
                 | 0 => x1
                 | S x2 => S (Ffix0 x2 x1)
                 end) x 0 :=
              match
                x as c
                return
                  (c =
                   (fix Ffix0 (x0 x1 : nat) {struct x0} : nat :=
                      match x0 with
                      | 0 => x1
                      | S x2 => S (Ffix0 x2 x1)
                      end) c 0)
              with
              | 0 => eq_refl
              | S x0 =>
                  match Ffix x0 in (_ = x1) return (S x0 = S x1) with
                  | eq_refl => eq_refl
                  end
              end) b in (_ = x) return (x = b)
         with
         | eq_refl => eq_refl
         end in (_ = x)
         return
           (S x =
            (fix Ffix (x0 x1 : nat) {struct x0} : nat :=
               match x0 with
               | 0 => x1
               | S x2 => S (Ffix x2 x1)
               end) b 1)
       with
       | eq_refl =>
           match
             plus_n_Sm b 0 in (_ = x)
             return
               (S
                  ((fix Ffix (x0 x1 : nat) {struct x0} : nat :=
                      match x0 with
                      | 0 => x1
                      | S x2 => S (Ffix x2 x1)
                      end) b 0) = x)
           with
           | eq_refl => eq_refl
           end
       end
     : forall b : nat, 1 + b = b + 1

Coq < Compute (plus_com 2).
     = fun b : nat =>
       match
         match
           match
             match
               (fix Ffix (x : nat) :
                  x =
                  (fix Ffix0 (x0 x1 : nat) {struct x0} : nat :=
                     match x0 with
                     | 0 => x1
                     | S x2 => S (Ffix0 x2 x1)
                     end) x 0 :=
                  match
                    x as c
                    return
                      (c =
                       (fix Ffix0 (x0 x1 : nat) {struct x0} : nat :=
                          match x0 with
                          | 0 => x1
                          | S x2 => S (Ffix0 x2 x1)
                          end) c 0)
                  with
                  | 0 => eq_refl
                  | S x0 =>
                      match Ffix x0 in (_ = x1) return (S x0 = S x1) with
                      | eq_refl => eq_refl
                      end
                  end) b in (_ = x) return (x = b)
             with
             | eq_refl => eq_refl
             end in (_ = x)
             return
               (S x =
                (fix Ffix (x0 x1 : nat) {struct x0} : nat :=
                   match x0 with
                   | 0 => x1
                   | S x2 => S (Ffix x2 x1)
                   end) b 1)
           with
           | eq_refl =>
               match
                 plus_n_Sm b 0 in (_ = x)
                 return
                   (S
                      ((fix Ffix (x0 x1 : nat) {struct x0} : nat :=
                          match x0 with
                          | 0 => x1
                          | S x2 => S (Ffix x2 x1)
                          end) b 0) = x)
               with
               | eq_refl => eq_refl
               end
           end in (_ = x) return (x = S b)
         with
         | eq_refl => eq_refl
         end in (_ = x)
         return
           (S x =
            (fix Ffix (x0 x1 : nat) {struct x0} : nat :=
               match x0 with
               | 0 => x1
               | S x2 => S (Ffix x2 x1)
               end) b 2)
       with
       | eq_refl =>
           match
             plus_n_Sm b 1 in (_ = x)
             return
               (S
                  ((fix Ffix (x0 x1 : nat) {struct x0} : nat :=
                      match x0 with
                      | 0 => x1
                      | S x2 => S (Ffix x2 x1)
                      end) b 1) = x)
           with
           | eq_refl => eq_refl
           end
       end
     : forall b : nat, 2 + b = b + 2

Coq < Compute (plus_com 1 2).
     = match plus_n_Sm 2 0 in (_ = x) return (3 = x) with
       | eq_refl => eq_refl
       end
     : 1 + 2 = 2 + 1

CC a écrit:

Il m'a plusieurs fois dit que le théorème de Timothy Griffith était pour lui la plus importante découverte depuis Godel

Christophe c a écrit:

le théorème classique, mais pas intuitionniste: $((A\to int) \to int)\to int$