Tarskian Interpretations with Infinite Domains

In TFF

• The Descedants problem

  [an error occurred while processing this directive]
       

Infinite term domains

• Use an infinite term domain

  tff(peano_type,type,       peano: $tType).
  tff(zero_decl,type,        zero: peano ).
  tff(s_decl,type,           s: peano > peano ).
  tff(peano2person_decl,type,peano2person: peano > person ).
  tff(peano_less_decl,type,  
      peano_less: ( peano * peano ) > $o ).
  
  tff(people,interpretation,
      ( ! [I: peano] : ( I = zero | ? [P: peano] : I = s(P) )
      & ! [I1: peano,I2: peano,I3: peano] :
          ( peano_less(I1,s(I1))
          & ( ( peano_less(I1,I2) & peano_less(I2,I3) )
           => peano_less(I1,I3) )
          & ( peano_less(I1,I2)
           => I1 != I2 ) )
      & ! [P: person] : ? [I: peano] : ( P = peano2person(I) )
      & ! [I1: peano,I2: peano] :
          ( peano2person(I1) = peano2person(I2) => I1 = I2 ) 

• Interpret problem terms and atoms

      & bob = peano2person(zero)
      & ! [I: peano] :
          child_of(peano2person(I)) = peano2person(s(I))
      & ( ! [A: peano,D: peano] :
            ( is_descendant(peano2person(A),peano2person(D))
          <=> peano_less(A,D) ) ) ) ). 

Integer domains

• Use a $int domain

  tff(int2person_decl,type, int2person: $int > person ).
  
  tff(people,interpretation,
      ( ! [P: person] : ? [I: $int] : P = int2person(I)
      & ! [I1: $int,I2: $int] : ( int2person(I1) = int2person(I2) => I1 = I2 ) 

• Interpret problem terms and atoms

      & bob = int2person(0)
      & ! [I: $int] : child_of(int2person(I)) = int2person($sum(I,1))
      & ! [A: $int,D: $int] : 
          ( is_descendant(int2person(A),int2person(D)) <=> $less(A,D) ) ) ).
       
  

Complete Examples

Descendants Play the Peano Terms

[an error occurred while processing this directive]

[an error occurred while processing this directive]

Descendants Count Integer Terms

[an error occurred while processing this directive]

[an error occurred while processing this directive]