Symbolic logic and AGI: explicit rules are not enough

Symbolic logic represents entities, relations, and rules through symbols whose use is fixed by a formal language. An engine can apply rules to facts or formulas and derive a conclusion: if “every drone carrying a heavy load must have its brakes checked” and this drone carries a heavy load, the check follows within the system. It does not follow that the sensor measured correctly, that the load is still on board, or that the rule covers every exception in the world.

That is both the value and the limit for a proposal about artificial general intelligence. A formal derivation can be inspected step by step; its validity depends on the chosen logic and supplied premises. Formalizing knowledge can be costly and brittle: McCarthy’s qualification problem shows that listing every condition for an action to succeed in advance can become impractical and still omit exceptions. Premise truth comes from somewhere else: people, sensors, databases, or learned models.

Three layers that must not be confused

Syntax determines which strings count as formulas. It defines the vocabulary, connectives, quantifiers, and formation rules. “P(a)” may be well formed even though nobody has said what “a” names or which property “P” expresses. A syntactically correct expression is not thereby true, useful, or provable. It is only a sentence admitted by the language.

Semantics supplies an interpretation. It fixes a domain of objects, what constants designate, and which objects or tuples satisfy each predicate. The Open Logic Project’s open introduction to first-order logic carefully separates formulas, the structures that interpret them, and the satisfaction relation that makes “true in a case” precise. Changing the interpretation can change the value of the same formula without altering a single symbol.

Proof belongs to a third layer. A proof system establishes which steps may take one formula to another. A sequence respecting those rules is a derivation; semantics determines whether the conclusion follows from the premises in every relevant model. Metatheory connects the two layers. A displayed list of steps is therefore not enough: one must know the rules, check each step, and know how those rules relate to the semantics.

Propositions and objects: what a quantifier buys

In propositional logic, a sentence such as “the sensor is active” is treated as a unit that can be true or false. Connectives can negate or combine units, but the language does not look inside them. The open text on propositional syntax and semantics defines valuations that assign true or false to variables and extend those values through truth tables. For a formula with finitely many variables, traversing all valuations gives a procedure that terminates.

First-order logic adds objects, predicates, relations, variables, and quantifiers. There is no need to mint a separate proposition for every drone. One can express that every object with certain properties obeys a rule, or that some object has those properties. This lets the language discuss entities and relations with a generality that propositional logic does not preserve.

Expressiveness has a cost. No method always terminates and decides whether every arbitrary first-order sentence is valid; the open treatment of the decision problem presents this through a reduction from the halting problem. This does not mean that no case can be solved. It means that “uses first-order logic” does not promise a universal decision procedure: practical systems restrict the language, accept searches that may not terminate, or use decidable fragments.

Soundness and completeness do not mean omniscience

A proof system is sound when every formula it derives from some premises is also a semantic consequence of those premises. It does not invent a conclusion beyond what the interpretation permits. It is complete when it can derive every semantic consequence expressible in the logic. The open summary of soundness and completeness states both directions: derivability implies consequence, and consequence implies derivability.

“Complete” does not mean that the system answers every question, possesses every fact, or finishes quickly. First-order logic has sound and complete proof systems, yet validity in general remains undecidable. Derivations can be enumerated until a proof of a valid formula appears; if the formula is not valid, that search may continue without returning “no.” Completeness is a relationship between semantics and proof, not a guarantee of efficiency.

Nor does it certify the world. From “every bridge in this database is open” and “the north bridge appears in the database,” one may derive that it is open. The deduction can be flawless while the first premise is out of date. A responsible application preserves the source and date of each premise, distinguishes observed data from supplied rules, and checks again whatever may have changed.

When a new fact should withdraw the conclusion

Consequence in classical logic is monotonic: if a conclusion follows from a set of premises, adding more premises does not remove that derivation. John McCarthy’s original discussion of the need for nonmonotonic reasoning explains both the syntactic and semantic property. A proof already constructed remains available in the enlarged set, even if the new information makes the theory inconsistent or useless for a decision.

Everyday life often relies on provisional conclusions. “Birds fly” supports an expectation that a newly encountered bird flies until one learns it is a penguin or is injured. The extra fact should not merely add the opposite conclusion beside the first; it should withdraw the default inference. Circumscription, default logics, and other nonmonotonic formalisms seek to represent that revision. They are not mistakes in logic; they change the consequence relation to handle incomplete knowledge.

Negation as failure is especially easy to misread. In a logic database, “not P” may be inferred when every permitted route for proving P fails. Keith Clark’s primary paper, Negation as Failure, ties that rule to the completed database and states conditions on queries and termination. “I could not prove it” does not simply become “it is false”: the move requires a closed-world assumption and a search whose failure has the defined meaning.

This detail changes an application. The absence of an allergy in a registry declared complete may support an operational rule; its absence from a partial medical history does not show that the allergy does not exist. Before accepting automated negation, ask which universe is treated as complete, which facts may arrive late, and what the system returns when a search does not terminate.

Symbolic and statistical are not rival teams

A statistical model learns regularities from examples and may generalize to inputs that were never written as rules. A symbolic system exposes vocabulary, premises, and steps, and can offer guarantees relative to that formalization. The former does not automatically provide a causal explanation; the latter does not automatically learn which symbols correspond to the world. Calling them “new versus old” hides that they solve different problems.

The survey Symbolic Logic meets Machine Learning scopes itself to the relationship between logic and learning, with an emphasis on infinite domains. Its own framework separates learning for logic, logic for learning, and methods crossing both. It supports that bridge; it is not a general source for every property of symbolic logic.

In a hybrid system, a learned component may recognize objects in an image while another component checks explicit planning constraints. Rules may also be learned, logical constraints may enter a loss function, or symbolic engines may operate over probabilistic predictions. The same survey of logic and learning in infinite domains shows that the boundary is not simply discrete versus continuous. The final guarantee depends on the interface: how a score becomes a symbol, which uncertainty is retained, and what the system does with a contradiction.

Verbal “reasoning” is not logical inference

A language model can produce a coherent chain of steps. That chain is generated text until somebody specifies a language, inference rules, and a verifier. Even a correct conclusion may be accompanied by a rationale that did not cause the answer or contains an invalid step. Fluency, length, and mathematical appearance do not create a proof.

A NeurIPS 2023 experimental study, Language Models Don’t Always Say What They Think, changed input features and observed plausible chain-of-thought explanations that omitted the biasing influence and rationalized predictions. Its test detects forms of unfaithfulness, but the authors warn that it cannot prove an explanation is faithful. The result does not say that a model never reasons; it says the text of its steps should not be treated as a certificate of its process by default.

A formal proof offers a different object: every step can be checked against declared rules. Even then, the verifier guarantees only the derivation within the system. It does not show that a natural-language sentence was translated correctly or that the premises describe the present. A model may propose a formalization and a checker may accept the proof; translation and premise provenance still require control.

How to audit a reasoning claim

Start by requesting four pieces: language, interpretation, premises, and inference mechanism. Are symbols assigned manually, extracted from text, or produced by a classifier? Is the logic classical, exception-tolerant, or based on a closed-world assumption? Is the output a checkable proof, an incomplete search, a score, or a generated explanation? If a demonstration cannot answer those questions, it has not yet identified the capability being shown.

Then build three cases. The ordinary one checks the expected path. The second preserves the form but supplies a false premise, revealing whether the system questions it or merely propagates it. The third adds a fact that should withdraw a provisional conclusion. Record which module detects the change, which source supports each premise, and whether the system distinguishes “false,” “unknown,” and “not provable.” Those outputs are not interchangeable.

To compare a symbolic, statistical, or hybrid proposal, hold the task and error cost constant. Measure generalization, deduction soundness, exception coverage, formalization cost, and traceability separately. A system may verify planning constraints or combine declared knowledge with a learned component, but winning on one of those axes does not establish general intelligence.

The transferable skill is separating syntax, semantics, and proof, then separating formal validity, premise truth, and learned capability. Explicit rules make an inference auditable; they do not make knowledge complete or turn the world into its model. When an AGI claim states which layer guarantees what, where conclusions can be withdrawn, and who verifies the facts, it stops leaning on the word “reasoning” and starts offering evidence.