To build and modify atoms, the syntactic pieces from which propositions are built up.

• §1. Elements and groups
• §5. Quantifiers
• §9. Unary predicates
• §10. Binary predicates
• §13. Validating atoms
• §14. Writing to text

§1. Elements and groups. Propositions are built up from "atoms": see What This Module Does for more. Those atoms are themselves pcalc_prop objects: what makes them atomic is simply that their next links lead nowhere yet.

define MAX_ATOM_ARITY 2

typedef struct pcalc_prop {
    int element;  one of the *_ATOM constants below: always 1 or greater
    int arity;  1 for quantifiers and unary predicates; 2 for BPs; 0 otherwise
    struct general_pointer predicate;  indicates which predicate structure is meant
    struct binary_predicate *saved_bp;  for problem messages only
    struct pcalc_term terms[MAX_ATOM_ARITY];  terms to which the predicate applies
    struct quantifier *quant;  QUANTIFIER_ATOM: which one
    int quantification_parameter;  QUANTIFIER_ATOM: e.g., the 3 in "all three"
    struct pcalc_prop *next;  next atom in the list for this proposition
} pcalc_prop;

• The structure pcalc_prop is accessed in 2/kp, 4/prp, 4/bas, 4/tcp, 5/sc, 5/smp and here.

§2. Each atom is an instance of an "element". There were never as many as 92 of these, but at one time the total was pushing 20, with many quasi-predicates having their own atom types. The introduction of Unary Predicate Families in 2020 simplified the picture considerably.

enum QUANTIFIER_ATOM from 1  any generalised quantifier
enum PREDICATE_ATOM          a regular predicate, rather than these special cases —
enum NEGATION_OPEN_ATOM      logical negation \(\lnot\) applied to contents of group
enum NEGATION_CLOSE_ATOM     end of logical negation \(\lnot\)
enum DOMAIN_OPEN_ATOM        this holds the domain of a quantifier
enum DOMAIN_CLOSE_ATOM       end of quantifier domain

§3. To handle the paired punctuation marks:

int Atoms::is_opener?Usage of Atoms::is_opener:
§13
Propositions - §2, §10, §31
Binding and Substitution - §1
Simplifications - §9.1, §9.2, §9.3, §9.3.1, §9.4, §13, §13.1(int element) {
    if ((element == NEGATION_OPEN_ATOM) || (element == DOMAIN_OPEN_ATOM))
        return TRUE;
    return FALSE;
}

int Atoms::is_closer?Usage of Atoms::is_closer:
§13
Propositions - §2, §10, §31
Binding and Substitution - §1
Simplifications - §9.1, §9.2, §9.3, §9.3.1, §9.4, §13, §13.1(int element) {
    if ((element == NEGATION_CLOSE_ATOM) || (element == DOMAIN_CLOSE_ATOM))
        return TRUE;
    return FALSE;
}

int Atoms::counterpart?Usage of Atoms::counterpart:
Propositions - §10, §31, §34(int element) {
    switch (element) {
        case NEGATION_OPEN_ATOM: return NEGATION_CLOSE_ATOM;
        case NEGATION_CLOSE_ATOM: return NEGATION_OPEN_ATOM;
        case DOMAIN_OPEN_ATOM: return DOMAIN_CLOSE_ATOM;
        case DOMAIN_CLOSE_ATOM: return DOMAIN_OPEN_ATOM;
        default: return 0;
    }
}

§4. Every atom is created by the following routine:

pcalc_prop *Atoms::new?Usage of Atoms::new:
§6, §9, §10
Propositions - §13, §16
Sentence Conversions - §2.13, §3.8
Simplifications - §2.2, §5, §6, §18, §19(int element) {
    pcalc_prop *prop = CREATE(pcalc_prop);
    prop->next = NULL;
    prop->element = element;
    prop->arity = 0;
    prop->predicate = NULL_GENERAL_POINTER;
    prop->quant = NULL;
    prop->saved_bp = NULL;
    return prop;
}

§5. Quantifiers. These have arity 1, and the single term must always be a variable, the one which is being bound.¹ The parameter is a number needed for some quantifier types to identify the range: for instance, it would be 7 in the case of Card= 7.

• ¹ Tying specific variables to quantifiers seems to be out of fashion in modern computer science. Contemporary theorem-proving assistants mostly use de Bruijn's numbering scheme, in which numbers 1, 2, 3, ..., refer to variables being quantified in an indirect way. The advantage is that propositions are easier to construct, since the same numbers can be used in different subexpressions of the same proposition, and there's no worrying about clashes. But it all just moves the difficulty elsewhere, by making it less obvious how to pair up the numbers with variables at compilation time, and less obvious even how many variables are needed. ↩

§6.

pcalc_prop *Atoms::QUANTIFIER_new?Usage of Atoms::QUANTIFIER_new:
Propositions - §16
Binding and Substitution - §10
Simplifications - §2.2, §3(quantifier *quant, int v, int parameter) {
    pcalc_prop *prop = Atoms::new(QUANTIFIER_ATOM);
    prop->terms[prop->arity++] = Terms::new_variable(v);
    prop->quant = quant;
    prop->quantification_parameter = parameter;
    return prop;
}

§7. Quantifier atoms can be detected as follows:

int Atoms::is_quantifier?Usage of Atoms::is_quantifier:
Propositions - §10
Simplifications - §13.1(pcalc_prop *prop) {
    if ((prop) && (prop->element == QUANTIFIER_ATOM)) return TRUE;
    return FALSE;
}

quantifier *Atoms::get_quantifier(pcalc_prop *prop) {
    if ((prop) && (prop->element == QUANTIFIER_ATOM)) return prop->quant;
    return NULL;
}

int Atoms::get_quantification_parameter(pcalc_prop *prop) {
    if ((prop) && (prop->element == QUANTIFIER_ATOM))
        return prop->quantification_parameter;
    return 0;
}

int Atoms::is_existence_quantifier?Usage of Atoms::is_existence_quantifier:
Propositions - §10, §29
Simplifications - §4, §6, §9.2, §13.1(pcalc_prop *prop) {
    if ((prop) && (prop->element == QUANTIFIER_ATOM) &&
        (prop->quant == exists_quantifier))
        return TRUE;
    return FALSE;
}

int Atoms::is_nonexistence_quantifier?Usage of Atoms::is_nonexistence_quantifier:
Simplifications - §9.2, §18, §19(pcalc_prop *prop) {
    if ((prop) && (prop->element == QUANTIFIER_ATOM) &&
        (prop->quant == not_exists_quantifier))
        return TRUE;
    return FALSE;
}

int Atoms::is_forall_quantifier?Usage of Atoms::is_forall_quantifier:
Simplifications - §18, §19(pcalc_prop *prop) {
    if ((prop) && (prop->element == QUANTIFIER_ATOM) &&
        (prop->quant == for_all_quantifier))
        return TRUE;
    return FALSE;
}

int Atoms::is_notall_quantifier?Usage of Atoms::is_notall_quantifier:
Simplifications - §18, §19(pcalc_prop *prop) {
    if ((prop) && (prop->element == QUANTIFIER_ATOM) &&
        (prop->quant == not_for_all_quantifier))
        return TRUE;
    return FALSE;
}

int Atoms::is_for_all_x?Usage of Atoms::is_for_all_x:
Propositions - §35(pcalc_prop *prop) {
    if ((Atoms::is_forall_quantifier(prop)) &&
        (prop->terms[0].variable == 0)) return TRUE;
    return FALSE;
}

§8. See Determiners and Quantifiers (in linguistics) for what a now-assertable quantifier is:

int Atoms::is_now_assertable_quantifier(pcalc_prop *prop) {
    if (prop->element != QUANTIFIER_ATOM) return FALSE;
    return Quantifiers::is_now_assertable(prop->quant);
}

§9. Unary predicates.

pcalc_prop *Atoms::unary_PREDICATE_new?Usage of Atoms::unary_PREDICATE_new:
Kind Predicates - §3, §4(unary_predicate *up, pcalc_term t) {
    pcalc_prop *prop = Atoms::new(PREDICATE_ATOM);
    prop->arity = 1;
    prop->terms[0] = t;
    prop->predicate = STORE_POINTER_unary_predicate(up);
    return prop;
}

unary_predicate *Atoms::to_adjectival_usage?Usage of Atoms::to_adjectival_usage:
Propositions - §30(pcalc_prop *prop) {
    return RETRIEVE_POINTER_unary_predicate(prop->predicate);
}

§10. Binary predicates.

pcalc_prop *Atoms::binary_PREDICATE_new?Usage of Atoms::binary_PREDICATE_new:
§11
Sentence Conversions - §2.13, §3.7
Simplifications - §3, §14(binary_predicate *bp,
    pcalc_term pt1, pcalc_term pt2) {
    pcalc_prop *prop = Atoms::new(PREDICATE_ATOM);
    prop->arity = 2;
    prop->predicate = STORE_POINTER_binary_predicate(bp);
    prop->terms[0] = pt1; prop->terms[1] = pt2;
    return prop;
}

binary_predicate *Atoms::is_binary_predicate?Usage of Atoms::is_binary_predicate:
Simplifications - §2, §7, §10, §11, §12(pcalc_prop *prop) {
    if (prop == NULL) return NULL;
    if (prop->element != PREDICATE_ATOM) return NULL;
    if (prop->arity != 2) return NULL;
    return RETRIEVE_POINTER_binary_predicate(prop->predicate);
}

int Atoms::is_equality_predicate?Usage of Atoms::is_equality_predicate:
§12
Propositions - §11, §26
Simplifications - §2, §6, §13, §16(pcalc_prop *prop) {
    binary_predicate *bp = Atoms::is_binary_predicate(prop);
    if (bp == R_equality) return TRUE;
    return FALSE;
}

§11. Given \(C\), return the proposition (x == C):

pcalc_prop *Atoms::prop_x_is_constant?Usage of Atoms::prop_x_is_constant:
Sentence Conversions - §4.3(parse_node *C) {
    return Atoms::binary_PREDICATE_new(R_equality,
        Terms::new_variable(0), Terms::new_constant(C));
}

§12. And conversely:

pcalc_term *Atoms::is_x_equals?Usage of Atoms::is_x_equals:
Sentence Conversions - §3.4(pcalc_prop *prop) {
    if (Atoms::is_equality_predicate(prop) == FALSE) return NULL;
    if (prop->terms[0].variable != 0) return NULL;
    return &(prop->terms[1]);
}

§13. Validating atoms.

char *Atoms::validate?Usage of Atoms::validate:
Propositions - §10(pcalc_prop *prop) {
    if (prop == NULL) return NULL;
    if (prop->arity > MAX_ATOM_ARITY) return "atom with overly large arity";
    if (prop->arity < 0) return "atom with negative arity";
    if (prop->arity == 0) {
        if (prop->element == PREDICATE_ATOM) return "predicate without terms";
        if (prop->element == QUANTIFIER_ATOM) return "quantifier without variable";
    } else {
        if ((prop->element != PREDICATE_ATOM) && (prop->arity != 1))
            return "unary atom with other than one term";
        if ((Atoms::is_closer(prop->element)) || (Atoms::is_opener(prop->element)))
            return "parentheses with terms";
    }
    if ((prop->element == QUANTIFIER_ATOM) && (prop->terms[0].variable == -1))
        return "missing variable in quantification";
    return NULL;
}

§14. Writing to text. Logging atomic propositions divides into cases:

void Atoms::log?Usage of Atoms::log:
Calculus Module - §3(pcalc_prop *prop) {
    Atoms::write(DL, prop);
}
void Atoms::write?Usage of Atoms::write:
Propositions - §7(text_stream *OUT, pcalc_prop *prop) {
    if (prop == NULL) { WRITE("<null-atom>"); return; }
    Use a special notation for equality14.1;
    switch(prop->element) {
        case PREDICATE_ATOM:
            switch(prop->arity) {
                case 1: Log some suitable textual name for this unary predicate14.2; break;
                case 2: Log some suitable textual name for this binary predicate14.3; break;
                default: WRITE("?exotic-predicate-arity=%d?", prop->arity); break;
            }
            break;
        case QUANTIFIER_ATOM: {
            quantifier *quant = prop->quant;
            Quantifiers::log(OUT, quant, prop->quantification_parameter);
            WRITE(" ");
            break;
        }
        case NEGATION_OPEN_ATOM: WRITE("NOT<"); break;
        case NEGATION_CLOSE_ATOM: WRITE("NOT>"); break;
        case DOMAIN_OPEN_ATOM: WRITE("IN<"); break;
        case DOMAIN_CLOSE_ATOM: WRITE("IN>"); break;
        default: WRITE("?bad-atom?"); break;
    }
    if (prop->arity > 0) {
        if (prop->element != QUANTIFIER_ATOM) WRITE("(");
        Log a comma-separated list of terms for this atomic proposition14.4;
        if (prop->element != QUANTIFIER_ATOM) WRITE(")");
    }
}

§14.1. Use a special notation for equality14.1 =

    if ((prop->element == PREDICATE_ATOM) && (prop->arity == 2) &&
        (RETRIEVE_POINTER_binary_predicate(prop->predicate) == R_equality)) {
        WRITE("(");
        Terms::write(OUT, &(prop->terms[0]));
        WRITE(" == ");
        Terms::write(OUT, &(prop->terms[1]));
        WRITE(")");
        return;
    }

• This code is used in §14.

§14.2. Log some suitable textual name for this unary predicate14.2 =

    unary_predicate *tr = RETRIEVE_POINTER_unary_predicate(prop->predicate);
    UnaryPredicateFamilies::log(OUT, tr);

• This code is used in §14.

§14.3. Log some suitable textual name for this binary predicate14.3 =

    binary_predicate *bp = RETRIEVE_POINTER_binary_predicate(prop->predicate);
    if (bp == NULL) WRITE("?bad-bp?"); else WRITE("%S", BinaryPredicates::get_log_name(bp));

• This code is used in §14.

§14.4. Log a comma-separated list of terms for this atomic proposition14.4 =

    for (int t=0; t<prop->arity; t++) {
        if (t>0) WRITE(", ");
        Terms::write(OUT, &(prop->terms[t]));
    }

• This code is used in §14.