Schemat

start

Schemat to twierdzenie drugiego rzędu używające zmiennych reprezentująxych formuły i termy. Schemat zaczyna się od słowa kluczowego scheme, Następnie jest lista parametrów czyli zmiennych drugiego rzędu, teza, która jest formułą i ewentualnie po słowie kluczowym provided przesłanki (także formuły). Np. schemat indukcji wygląda następująco

scheme :: NAT_1:sch 1
   Ind { P[ Nat] } :
   for k being Element of NAT holds P[k]
provided
A1:  P[ 0 ] and
A2:  for k being Element of NAT st P[k] holds P[k + 1];
end;

Użycie schematu:

defpred Q[Nat] means Φ($1);
A5: Q[0]
  proof
      ....... 
  end;
A6: for n being Element of NAT st Q[n] holds Q[n+1]
  proof
    ...............
  end;
  for n being Element of NAT holds Q[n] from NAT_1:sch 1(A65A6);