It will be easier if I present the motivation in order to express the question better.

Creating shorthand symbols for long sentences/propositions/assertions is ubiquitous. Many authors do it everywhere, then also then use it -both trivially and usefully. But it is also quite obvious that real utility is when I can manipulate on these symbols, instead of using them for purely denotational purposes (trivial usage). In short, it will be agreed that creating new unique shorthand for every proposition isn't very useful (there being no point). In fact, what is required is a sort of full generality from a fixed system.

More concretely, if I were to create a new system (for some purpose, say I am a mathematician, and I want to theorise this exotic object I have invented), how do I make sure my theory is "reasonable" (capable of new theorems) ? And what has this got to do with, say, first order logic, or any logic? I can almost sense I am hitting on completeness theorem, but not sure how to connect it to my question.

So what makes one system of syntax capable of being reasonably (usefully) computable?

Note: Focus here is not on Turing machines' computability, but on the notion of reasonable computability, which is, incidentally, captured by Turing machines. (TM can implement non-sensible systems too). Of course, a useful system must be "useful" in mathematical, scientific work.


6 Answers 6


You seem to refer to Formal Systems. A formal system is essentially a set of concepts (precise definition of objects) and axioms (atomic principles, which in the context of the current system cannot be decomposed anymore) that allow further logical calculus.

Notice that the term formal confers two meanings in this context: a) the system has logical consistency; b) the system is expressed in a written form, which is very important: Logic and Reason are essentially the expression of the rules of thinking, the difference between them is that while Logic is the formal expression, that is, a set of written rules, Reason is the process of thinking, and it is not a formal system. So, you base your system not only upon Reason -the rules of thinking, which includes logical fallacies and other cognitive biases-, but also upon Logic -which tends to exclude logical flaws, mainly because it is properly organized and expressed in written form-.

The core formal system of all Physics and Metaphysics is Logic (and specifically, Propositional Logic). You can build whatever formal system upon it (e.g. Thermodynamics, or Chess, any of which allow further calculations), but you can't decompose Logic. Any attempt to decompose Logic ends up in the development of tautologies (e.g. Logic is true is a logical rule, that cannot confer any logical validity to Logic, except when it is already possible by means of Logic).

So what makes one system of syntax capable of being reasonably (usefully) computable?

As you've probably already noticed, the quality that provides validity to your formal system will be logical consistency. If your system is logically consistent, and has no contradictions (so that the Principle of Explosion cannot destroy it), it would be enough to build upon any further calculus and even new formal systems.

Note: Focus here is not on Turing machines' computability, but on the notion of reasonable computability, which is, incidentally, captured by Turing machines.

Perfect, because you either base your formal system upon plain Logic (e.g. so you can build a game, like rock, scissors, paper), or you base it upon Turing Machines (so you can create a new formal system based upon the rules of Turing Machines, like the Assembly programming language).

  • Thanks for answering! I'm not quite sure - how does a formal system capture logic? For once we have a formal logical system in place, appeal to intuition is essentially redundant. That whatever is logical is taken care by the system. And then you can show "completeness", "undecidability", etc. of the logic. So how does a formal system formalise logic?
    – Ajax
    Commented Feb 26 at 9:56
  • 1
    @Ajax 1) "how does a formal system capture logic?"/"how does a formal system formalise logic?": It does not, because it depends on logic (e.g. 2nd Law of Thermodynamics: ΔS>0 does not "capture logic", it is just a logical axiom). 2) "whatever is logical is taken care by the system": False: a formal system can hold contradictions and illogical axioms. Examples are a) Euclidean Geometry, which was demonstrated to be inconsistent, so Non-Euclidean Geometries were introduced to solve the problem; b) Thermodynamics held contradictions solved by the introduction of the zero-th Law, etc.
    – RodolfoAP
    Commented Feb 26 at 12:06

To me it sounds like you are asking some ill-formed questions that could be clarified if you were familiar with some basic concepts. You say the following:

how do I make sure my theory is "reasonable" (capable of new theorems) ? And what has this got to do with, say, first order logic, or any logic?

A useful system is where we can deduce new propositions - at least one which is useful in mathematical and scientific investigations.

Ok, let's work within FoL -I define a mathematical object, I give it a name, and perhaps define a thing or two more. Then perhaps one more.... At what stage does this mathematical theory T become "computable" - so that I can ask mathematicians, "go ahead, prove theorems in theory T"? Can it happen that they end up saying, "your theory cannot prove any theorem -it is broken!"? or perhaps they say, "your theory T is too minimalistic as of now, define something more!". Basically, my theory T is technically incapable of supporting theorem proving. So is there a "cutoff" when theory becomes capable of supporting theorem proving?

It's important to keep separated ideas in the system you are working in, and concepts about the system (meta theory), and more "human readable" explanations of these ideas. Often there is an amount of "translation" that occurs.

∀x (0 ≠ S(x))

compared to "zero is not the successor of any number." Or consider the first order induction definition in Peano Arithmetic; this is quite lengthy and complex in first order logic, but much easier to talk about here in the meta theory.

Secondly, formal systems are built up from axioms. The 20th century saw a lot of mathematical interest in considering what was possible to prove or not prove starting with various axioms. Towards the end of the century Reverse Mathematics was established to evaluate the opposite direction, asking what (minimal) axioms are needed to prove some theory or other.

So for your idea about theorem proving, this is really always available because formal systems start with axioms. And really you don't need much to start asking what theorems follow from which axioms, because these are just substitution/replacement rules. Take a look at some related tool like Metamath. From a given set of axioms, it will perform replacements until a result is established (your theorem is proved).

A minor response to "your theory T is too minimalistic as of now, define something more". For a practical example, it might be helpful to consider Presburger arithmetic, Robinson arithmetic, and maybe Peano arithmetic. It's not important to understand the details, I just want to point out that these have similar axiom systems. Presburger and Robinson arithmetic both use different subsets of axioms from Peano arithmetic. However, Presburger arithmetic is decidable while Robinson arithmetic is not. Your original question is not really well-formed, but this sort of shows the difference in how a set of axioms is "too minimalistic" (but still interesting) compared to a different set of axioms.

  • Thanks for answering. Would you say that completeness (from Godel's Completeness Thm) of FoL is the major reason that our mathematical theories work?
    – Ajax
    Commented Feb 26 at 17:56
  • 1
    No. Some "mathematical theories" are derivable in FoL and some are not. And from the Incompleteness Theorem we know some true things are not provable. Really that's kind of beside the point of whether they "work" or not (~ practical engineering applications).
    – BurnsBA
    Commented Feb 26 at 18:12

Define your new symbols in terms of your old symbols. Pay attention to grammatical class; your new symbols should have the same class as the productions which they represent.

Then, you only have to add two rules per new symbol: one to encode the new symbol and one to decode it.

This also works for parameterized productions, as long as the grammatical classes of the parameters match.

Edit for posterity: Here is a quote from Metamath's notes on definitions which may be clearer about exactly what is required:

A definition is sound provided (1) it is eliminable (the wff for any theorem containing a defined symbol can be converted to an equivalent wff without it) and (2) it is conservative (a theorem should be provable from the original axioms after the definition is eliminated).


You can start by considering examples of reasoning within the reasoning domain you're targeting. Examples of the form, "from X and Y, Z would follow."

Generate a lot of these examples. Be creative. Consider the edge cases.

Then look hard at them and ask yourself if you can think of any exceptions, where X and Z might occur but Z would not follow. If you can think of any exceptions, you can't formalize that reasoning. Instead sit back and try to think of a more general rule, accounting for more information in the premises. Perhaps "from X and Y and W, Z follows," would work without any exceptions.

You need to be sure there are no exceptions in your examples before you can proceed.

Once you have your examples of reasoning without any exceptions, you can try to look for general rules that yield the examples as special cases. Keep adding more examples, trying to find ones that contradict the general rules you're thinking about. If a general rule is contradicted, you'll need to throw it out, amend it, or decide on some reinterpretation of terms that would make the contradicting example invalid, or make an extra assumption or simplification that means you're no longer trying to model that type of contradiction.

Keep going for a long time, looking for contradictions in your examples and general rules.

When you're convinced that everything follows necessarily from the premises, given your assumptions and the limited scope of situations you've decided to model, then you can write down some symbols to represent the general rules more concisely.

It also is helpful to try to mimic the form of existing mathematical systems. For example, if you can write your ideas as a system of differential equations, then you know you can do math with that. Or maybe a cellular automaton, or a finite state machine, or statistical regression. Try to think of what in mathematics is most like what you're trying to model.

Also, temper your expectations. You're asking for valid, deductive reasoning, in which the conclusion follows necessarily from the premise. Such reasoning appears in logic and math. However, when we're talking about the real world, or most philosophy, the vast majority of reasoning is not like this. The conclusions only follow approximately and probably from the premises.


You ask:

So what makes one system of syntax capable of being reasonably (usefully) computable?

I'm not sure that I can find a source for what makes a good formal system, however, here are some suggested traits:

  1. The abstraction to a simpler syntax is done well. Natural language constructions are complex. The ability to reduce a compound complex sentence to a single letter in propositional logic allows one to see a structure like modus ponens in a single glance, for example.

  2. The simpler syntax means emphasizes the important aspect of the semantics. Formal semantics comes in an astounding variety of, well, shapes. It includes logical semantics, arithmetical semantics, computational semantics, linguistic semantics, etc. Each of those can be emphasized by a good syntax.

  3. The formal system disambiguates and precises the constructions well. Both ambiguity and vagueness are inherent to language. By simplifying natural language which is usually reserved as a metalanguage for describing the metatheory, it allows the use of a simplified artificial language created by consensus generally on pragmatic grounds instead. Linguists, computer scientists, mathematicians, and logicians use such formal systems as a lingua franca.

  4. The formal system should enable automation of computation. Modern mathematics, might, for instance, rely on the use of the Calculus of Constructions for a proof. Mathematicians used to used sticks to draw in the sand; now they upload the problem definition and set theorem provers to task.

  5. The syntax should simplify the grammar of the metatheory if posssible. Grammars comes in flavors described by a scheme called the Chomskian hierarchy. A formal system mike be simple like a language for regular expressions, or it might purport to handle the full complexity of natural languages. In CS, the use of context-free grammars is a big win because it allows a linearization of a directed acyclic graph which allows for a deterministic outcome in dealing with a data structure.

  6. To be reasonable, the formal syntax should be clear, compositional, and comprehensible. That is, if there are mathematical parts, those should use a well-accepted mathematical formalism, and if there are logical parts or computational or linguistic formalisms, the syntax should borrow from those as well. And all of the metatheories should be interwoven and simplified so that coming into the syntax should, in an ideal world, be accessible by self-study.

That's what comes to mind at first glance, anyway. Outside of this, a formal system is a tool, and so whatever makes a tool useful, is what makes an artificial syntax useful.


So what makes one system of syntax capable of being reasonably (usefully) computable?

Any logical language whose logic you understand and whose vocabulary means real things.

So you need to understand what each word in this language means, and to know the (complete) syntax, which is to say, you need to know all the rules of the syntax.

You also need a good programmer.

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .