Interpreting TNT Formulas in Finite Domains
Here is a program that interprets formulas of Typographical Number
Theory (TNT) in finite domains; specifically, in the domain of
integers modulo N, where N is an arbitrary natural number.
Note that this interpretation is not a model for the set of
TNT theorems; for example, the first axiom, "Aa:~Sa=0", is false under
this interpretation.
The program is meant to illustrate
Tarski's definition of truth for formalized languages
.
One can define predicates using the
square-bracket substitution notation
and build new predicates out of previously defined predicates; these
features demonstrate the close analogy between TNT and a computer
programming language.
The program can also interpret formulas in the domain of natural
numbers by restricting the quantifiers so that they only range over
the numbers 0 to N-1, where N is an arbitrary natural number (strictly
speaking, this is not an interpretation in Tarski's sense of the
word because the quantifiers do not range over the entire domain).
With some care, this feature can be used to help determine whether a
formula is true when interpreted in the domain of natural numbers.
Files
-
tarski.c
-
Interpret TNT formulas in finite domains.
The program can run interactively by not specifying any command
line arguments, or it can process an input file containing a list of
commands by specifying the input filename as a command line argument.
-
example.in,
example.out
-
Example input file.
This file illustrates various features of the program.
-
power.in,
power.out
-
Example input file.
This file checks the components of my solution to one of Hofstadter's
translation puzzles by interpreting formulas in a domain of natural
numbers with restricted quantifiers.
Commands
One can set the domain of interpretation by using the following
commands:
- :zN
-
This command sets the domain of interpretation to ZN, the
integers modulo N, where N is an arbitrary natural number.
- :nN
-
This command sets the domain of interpretation to the natural
numbers with quantifiers ranging over the numbers 0 to N-1, where N is
an arbitrary natural number.
|