Truth Theory¶

This module is mostly exploratory, I did it for fun, to see if something could be done.

Languages¶

class logics.classes.predicate.language.TruthPredicateLanguage(individual_constants=None, individual_metavariables=None, variables=None, variable_metavariables=None, quantifiers=None, metavariables=None, constant_arity_dict=None, predicate_letters=None, predicate_variables=None, function_symbols=None, sentential_constants=None, allow_predicates_as_terms=False)¶

Language for arithmetic containing a truth predicate

Subclasses PredicateLanguage but has a special clause for is_well_formed, which states that atomic formulae that begin with predicate 'Tr' must have a numeral as its only argument. I.e. truth predicate atomics must be of the form PredicateFormula(['Tr', '514951'])

Instances¶

logics.instances.predicate.languages.arithmetic_truth_language¶: A language for arithmetic truth. Similar to the language of natural number arithmetic (see Language > Instances), with added unary predicate Tr, unary function quote and sentential constant λ.

Parsing utilities¶

Godel encoding and decoding is handled by the parser.

logics.utils.parsers.parser_utils.godel_encode(string)¶

Godel encoding function for the language logics.instances.predicate.languages.arithmetic_truth_language

Codes an unparsed sentence (the string you would give to the parser). Works as follows:

Constant "0" is represented by 0
Auxiliary symbols begin with 1 (e.g. "(" is 19, ")" is 199)
Connectives begin with 2 (e.g. "~" is 29, "∧" is 299, "∨" is 2999)
Quantifiers begin with 3 (e.g. "∀" is 39, "∃" is 399)
Predicates begin with 4 (e.g. "=" is 49, "Tr" is 49999)
Variables with 5, Predicate variables with 6 (e.g. "x" is 51, "x1" is 519, "X" is 61)
Metavariables and sentential constants begin with 7 (e.g. "A" is 79, "λ" is 79999)
Function symbols begin with 8 (e.g. "s" is 89, "+" is 899)

Returns: The numeral representing the Godel number of the sentence
Return type: str
Raises: logics.classes.exceptions.NotWellFormed – If it detects a character that is none of the above. Note that whitespace is taken as non-recognized.

Examples

>>> from logics.utils.parsers.parser_utils import godel_encode
>>> godel_encode('0=0')
'0490'
>>> godel_encode('0 = 0')
Traceback (most recent call last):
...
logics.classes.exceptions.NotWellFormed: Non-recognized character   in Godel encoding
>>> godel_encode('s(0)+s(0)=s(s(0))')
'891901998998919019949891989190199199'
>>> godel_encode('1+1=2')  # Remember that arithmetic has only 0 as individual constant
Traceback (most recent call last):
...
logics.classes.exceptions.NotWellFormed: Non-recognized character 1 in Godel encoding
>>> godel_encode('∀x(~0=0)')
'395119290490199'
>>> godel_encode('forall x (0=0)')
Traceback (most recent call last):
...
logics.classes.exceptions.NotWellFormed: Non-recognized character f in Godel encoding

Notes

You will probably not need to call this function directly, the parser will call it for you, see below.

logics.utils.parsers.parser_utils.godel_decode(string)¶

Godel decoding function for the language logics.instances.predicate.languages.arithmetic_truth_language

Reverses the function above.

Examples

>>> from logics.utils.parsers.parser_utils import godel_decode
>>> godel_decode('0490')
'0=0'
>>> godel_decode('891901998998919019949891989190199199')
's(0)+s(0)=s(s(0))'
>>> godel_decode('395119290490199')
'∀x(~0=0)'

class logics.utils.parsers.predicate_parser.ArithmeticTruthParser(godel_encoding_function, godel_decoding_function, *args, **kwargs)¶

Parser for arithmetic truth

Subclasses PredicateParser, but does Godel coding of things inside Tr predicate

Parameters

godel_encoding_function (callable) – The function with which you wish to encode sentences inside Tr predicates
godel_decoding_function (callable) – The function with which you wish to decode sentences inside Tr predicates
everything_else_in_PredicateParser – Everything else present in the parent PredicateParser class

Examples

>>> from logics.instances.predicate.languages import arithmetic_truth_language
>>> from logics.utils.parsers.parser_utils import godel_encode, godel_decode
>>> from logics.utils.parsers.predicate_parser import ArithmeticTruthParser
>>> replacement_dict = {
...     '¬': '~', 'not ': '~',
...     '&': '∧', ' and ': '∧',  # notice the spaces before and after 'and'
...     'v': '∨',  ' or ': '∨',
...     ' then ': '→', '-->': '→', 'if ': '',  # 'if p then q' it will convert to 'p then q'
...     ' iff ': '↔', '<->': '↔',
...     'forall ': '∀', 'exists ': '∃', ' in ': '∈'
... }
>>> replacement_dict.update({
...     '⌜': 'quote(',
...     '⌝': ')'
... })
>>> arithmetic_truth_parser = ArithmeticTruthParser(godel_encoding_function=godel_encode,
...                                                 godel_decoding_function=godel_decode,
...                                                 language=arithmetic_truth_language,
...                                                 parse_replacement_dict=replacement_dict,
...                                                 infix_cts=['∧', '∨', '→', '↔'],
...                                                 infix_pred=['=', '<', '>'], infix_func=['+', '*', '**'])
>>> arithmetic_truth_parser.parse('0=0+0')
['=', '0', ('+', '0', '0')]
>>> arithmetic_truth_parser.parse('Tr(⌜0=0+0⌝)')
['Tr', '04908990']
>>> arithmetic_truth_parser.parse('Tr(⌜Tr(⌜0=0⌝)⌝)')
['Tr', '4999919899999190490199199']
>>> arithmetic_truth_parser.parse('λ iff ~Tr(⌜λ⌝)')
['↔', ['λ'], ['~', ['Tr', '79999']]]

Instances¶

logics.utils.parsers.predicate_parser.arithmetic_truth_parser¶: Identical to the instance defined in the example above.

Model theories¶

class logics.classes.predicate.semantics.models.TruthPredicateModelTheory(parser, *args, **kwargs)¶

Model theory class for systems with a truth predicate

Subclasses from ModelTheory. Has two changes from it:

Sentential constants can now denote formulae instead of truth values. If it finds a constant like that, the valuation of the constant will equal the valuation of the denoted sentence
Modifies the atomic valuation clause in case of an atomic beginning with Tr. In that case it will decode the sentence using the parser provided and evaluate it

Parameters

parser (logics.utils.parsers.predicate_parser.ArithmeticTruthParser) – The parser you wish to use, to decode sentences inside Tr predicates
everything_else_in_ModelTheory – Everything else in ModelTheory

liar_sentence¶

The predicate formula representing the liar sentence (for convenience, so that you can do model_theory.liar_sentence). By default it is PredicateFormula(['λ'])

Type: logics.classes.predicate.PredicateFormula

Examples

>>> from logics.utils.parsers.predicate_parser import arithmetic_truth_parser
>>> from logics.instances.predicate.languages import arithmetic_truth_language
>>> from logics.instances.predicate.model_semantics import predicate_classical_truth_functions
>>> from logics.classes.predicate.semantics.models import TruthPredicateModelTheory
>>> # Sentence λ denotes its own negation
>>> sent_constants = {'λ': arithmetic_truth_parser.parse('~Tr(⌜λ⌝)')}
>>> arithmetic_truth_model_semantics = TruthPredicateModelTheory(parser=arithmetic_truth_parser,
...                                                 language=arithmetic_truth_language,
...                                                 truth_values=['1', '0'], designated_value='1',
...                                                 truth_function_dict=predicate_classical_truth_functions,
...                                                 sentential_constant_values_dict=sent_constants,
...                                                 use_molecular_valuation_fast_version=True,
...                                                 use_quantifier_fast_version=True)

With this, we can evaluate sentences containing the truth predicate:

>>> from itertools import count
>>> from logics.instances.predicate.model_subclasses import ArithmeticModel
>>> standard_model = ArithmeticModel({'domain': count(0)})
>>> arithmetic_truth_model_semantics.valuation(arithmetic_truth_parser.parse('Tr(⌜0=0+0⌝)'), standard_model)
'1'
>>> arithmetic_truth_model_semantics.valuation(arithmetic_truth_parser.parse('Tr(⌜Tr(⌜0=0⌝)⌝)'), standard_model)
'1'

And what you are now surely wondering:

>>> arithmetic_truth_model_semantics.valuation(arithmetic_truth_model_semantics.liar_sentence, standard_model)
Fatal Python error: Cannot recover from stack overflow.

Basically what happens is:

The atomic clause for valuation is called with the sentence λ
It sees that it is a sentential constant so it looks up what it denotes
It sees that it denotes a formula, namely, ~Tr(⌜λ⌝), so it recursively calls valuation with it
valuation is called with ~Tr(⌜λ⌝). It enters the negation clause, which calls valuation recursively in order to return the flipped value
valuation is called with Tr(⌜λ⌝). It enters the truth predicate clause of the atomic case. This decodes ⌜λ⌝ (which it internally sees as ‘79999’) to λ, and evaluates it
Goes back to step 1 of the process

This should raise a RecursionError but is currently giving me a stack overflow (I’m not sure why). But even if that worked, it wouldn’t be very satisfactory, because it would give us the same error with any self-referential sentence even if it is not a problematic one. One thing we could try is to build some sort of kripkean fixed-point apparatus to deal with this. I leave it as future work.

Instances¶

logics.instances.predicate.model_semantics.arithmetic_truth_model_semantics¶: Identical to the instance defined in the example above.