Non-classical Logics

by Tobias Gleißner, Alexander Steen, Geoff Sutcliffe, Christoph Benzmüller

Motivation

Extension of the TPTP TXF and THF dialects to support a wide range of non-classical logics with

Minimal syntactic changes
User-friendly syntax (easy reading and writing of problems)
Developer-friendly syntax (easy parsing, minimal cases to consider e.g., when defining semantics)
Uniform syntax for all non-classical logics
Consistency throughout TPTP dialects

Overview

A long form for all connectives of any non-classical logic. The long form contains the full name of a connective as defined words e.g. $permissible.
A short form for selected connectives in selected non-classical logics, e.g., [.] and <.> for $necessary and $possible in alethic modal logic.
A seperate specification of the semantics.

The descriptions and examples below are in terms of alethic modal logic. The syntax offers much more - see the section on the exotic future below.

Connectives Long Form

Non-classical connectives belonging to a logic get unique defined names, e.g., $necessary. The connectives are written in {} brackets (to indicate that they are non-classical, and their semantics has to be defined in a semantics specification). System names may also be used for user-defined connectives, e.g., {$$canadian_conditional}, thus allowing use of the TPTP syntax when experimenting with logics that have not yet been formalized in the TPTP. They are used in prefix form, with the arguments in ()s for TXN, and applied using @ in THN. The BNF grammar is here.

Examples:

    tff(pigs_might_fly_type,type,pigs_might_fly: $o ).

    tff(no_flying_pigs,axiom,
        ~ ({$possible} @ (pigs_might_fly) ) ).

    tff(something_is_possible,axiom,
        ? [P: $o] : {$possible} @ (P) ).

    thf(forbidden_flying_pigs,axiom,
        {$forbidden} @ pigs_might_fly ).

    thf(everything_is_permissible,axiom,
        ! [P: $o] : ( {$permissible} @ P ) ).

Connectives may have a list of parameters, where a parameter is one of:

A optional single initial index term starting with #. The index can be any constant (uninterpreted constant, number, TPTP defined constant) of any type. The TPTP might provide predefined values, e.g., $past, for individual logics. Indices are distinct from each other and from object logic terms. Examples:

    tff(an_individual_type,type,me: $i ).

    tff(for_me_it_is_possible,axiom,
        {$possible(#me)} @ (pigs_might_fly) ).

    tff(for_me_something_is_possible,axiom,
        ? [P: $o] : {$possible(#me)} @ (P) ).

    thf(agent_type,type,agent: $tType ).

    thf(archer_type,type,archer: agent ).

    thf(archer_knows_flying_pigs,axiom,
        {$knows(#archer)} @ pigs_might_fly ).

    thf(for_archer_everything_is_permissible,axiom,
        ! [P: $o] : ( {$permissible(#archer)} @ P ) ).

A key-value expression of form LHS := RHS where LHS is a TPTP defined constant, and RHS is a term (for TFF a tff_atomic_formula, for THF a thf_fof_function). This is not used in alethic modal logics, but in other logics, e.g., epistemic logic ...
```
    {$knows(#1)}({$common($group:=[2,3,4])}(something_commonly_known_by_agents_2_3_and_4))
     
```

Connectives Short Form

The short forms provide shorthand for the long forms. Two short forms are available in alethic modal logics: [...], <...>. The short forms are associated by TPTP standards with specific long forms in specific logics, e.g., in alethic modal logic [...] is short for {$necessary:...} and <...> is short for {$possible:...}. There might not be a short form for every long form in a given logic. The short forms may be parameterized by an index, but nothing more. A non-indexed short form has a period in the brackets. The BNF grammar is here.

Examples:

    tff(no_flying_pigs,axiom,
        ~ (<.> @ (pigs_might_fly) ) ).

    tff(for_me_it_is_possible,axiom,
        <#me> @ (pigs_might_fly) ).

    thf(forbidden_flying_pigs,axiom,
        <.> @ pigs_might_fly ).

    thf(archer_knows_flying_pigs,axiom,
        [#archer] @ pigs_might_fly ).

Short forms and long forms can be used together, e.g., it’s OK to use {$necessary} and [.] in the same problem or formula.

Semantics Specification

Annotated formulae with the (new) role logic are used to specify the semantics of the logic. Such a formula begins with the keyword for the logic, e.g., $modal, $alethic_modal, $deontic_modal, $epistemic_modal, followed by == and a list of properties value assignments. Each specification is the property name, followed by == and either a value or a tuple of specification details. If the first element of a list of details is a value, that is the default value for all cases that are not specified in the rest of the list. Each detail after the optional default value is the name of a relevant part of the vocabulary of the problem, followed by == and a value for that named part. The BNF grammar is here.

The semantic specification typically comes first in a problem file. A logic specification changes the meaning of things such as the boolean type $o, universal quantification with !, etc. Their existing meaning in classical logic should not be confused with the meaning in the declared logic.

For alethic modal logics the properties that may be specified are $constants, $quantification, and $modalities. The $constants, $quantification, and $modalities may have individual values for constants and types.

$constants
- $rigid - Rigid constants are independent of worlds.
- $flexible - Flexible constants are dependent on worlds.
$quantification
- $constant - Constant domain semantics has all world's domains fixed the same.
- $varying - Varying domain semantics has (potentially) different domains for each world.
- $cumulative - Cumulative domain semantics and varying, and the domain of each world is a superset of the domains of the worlds from which it can be reached.
- $decreasing - Decreasing domain semantics and varying, and the domain of each world is a subset of the domains of the worlds from which it can be reached.
$modalities - These are specified in this Wikipedia page.
- A known system name may be given, as listed in LOG001_4.l.
- A tuple of known axiom names may be given, as listed in LOG001_3.l.

The formulae of a problem can be either local (true in the current world) or global (true in all worlds). By default formulae with the roles {\tt hypothesis} and {\tt conjecture} are local, and all others are global. These defaults can be overridden by adding a subrole, e.g., {\tt axiom-\$local}, {\tt conjecture-\$global}.

See CorrectSpecifications.p for examples. The grammar is not very restrictive on purpose, to enable working with other logics as well. It is possible to create a lot of nonsense specifications, and to say the same thing in different meaningful ways. A tool to check the sanity of a specification is available.

TPTP Logics

Logic	Name	Connectives	Semantics
Generic modal	`$modal`	`$box`, `$dia`	`$modal == [ $constants == C, $quantification == Q, $modalities == M ]` `C ∈ { $rigid, $flexible }` `Q ∈ { $constant, $varying, $cumulative, $decreasing }` `M == $modal_system_Sys \| [ $modal_axiom_Ax₁, $modal_axiom_Ax₂, ... ]` `Sys ∈ { K,KB,K4,K5,K45,KB5,D,DB,D4,D5,D45,T,B,S4,S5,S5U }` `Ax ∈ { K,T,B,D,4,5,CD,BoxM,C4,C }`
Alethic modal	`$alethic_modal`	`$necessary`, `$possible`	`$alethic_modal ==` as for `$modal`
Deontic modal	`$deontic_modal`	`$obligatory`, `$permissible`, `$forbidden`	`$deontic_modal ==` as for `$modal`
Epistemic modal	`$epistemic_modal`	`$knows`, `$canKnow`	`$epistemic_modal ==` as for `$modal`
Doxastic modal	`$doxastic_modal`	`$believes`, `$canBelieve`	`$doxastic_modal ==` as for `$modal`
Temporal (instant-based)	`$temporal_instant`	`$future`, `$past`, `$henceforth`, `$hitherto`	`$temporal_instance == [ $constants == C, $quantification == Q, $modalities == M, $time == T ]` `C and Q` as for `$modal` `M == [ $modal_axiom_AxTm₁, $modal_axiom_AxTm₂, ... ]` `Ax ∈ { K,T,B,D,4,5 }` `Tm ∈ { +,- }` `T ∈ { $reflexivity, $irreflexivity, $transitivity, $asymmetry, $anti_symmetry, $linearity, $forward_linearity, $backward_linearity, $beginning, $end, $no_beginning, $no_end, $density, $forward_discreteness, $backward_discreteness }`

Examples

These examples can be run in Leo-III within SystemOnTPTP. Leo-III embeds non-classical logic problems into plain THF, and solves the THF problem. The embedding tool is available as Logic2THF in SystemB4TPTP, the output from which can be given to any THF system.

Logic Documentation

The various logics, the syntax used, the axiom schemes, and the semantics specification, are being semi-formally documented in a machine readable form. This work is available in the Logics directory of the Github repository.

Exotic Future

The use of the TPTP framework for non-classical logics, as presented so far, is conservative, adopting only widely accepted structures in alethic modal logics. The TPTP framework is capable of much more. Some of our ideas are listed here, some relevant and unpolished files are in the ExoticFuture directory, and feedback is welcome.

Using object logic terms, including variables, as indices.
Non-alethic modal logics are already supported in the syntax, and tool support will be added.
Encoding of description logic (ALC, ALCQI) problems in TPTP description logic format (an old TPTP effort) into modal logic.
Two more short forms {...}, and (...).
In logic specifications that $modalities may be written as THF formulae, or as frame conditions using $r as the accessibility relation.
Problems with multiple logics together. (Short forms may not be used when multiple logics are used together - the long forms have to be used, to avoid conflicting uses of the short forms.)
Problems with semantics templates that represent multiple semantics specifications, and a tool to burst these out into individual problem files.
More (non-modal) logics.
More and more