# Questions tagged [formal-systems]

A formal system is broadly defined as any well-defined system of abstract thought based on the model of mathematics. (Def: http://en.m.wikipedia.org/wiki/Formal_system)

40 questions
47 views

### What is a gross-looking formal axiomatic proof for a relatively simple proposition?

I'm looking for long and hard to follow derivations or symbolic proofs to motivate how tedious it is to actually reason within a formal system. I'm hoping there is an image of the proof, with few if ...
821 views

### Understanding definition of conservative extension of a theory

From Wikipedia In mathematical logic, a logical theory $T_2$ is a (proof theoretic) conservative extension of a theory $T_1$ if the language of $T_2$ extends the language of $T_1$; every ...
235 views

### The monadic second order theory with $<$ and Presburger arithmetic

Consider the monadic second order logic over the natural numbers with $<$ as a predicate, i.e. the second order logic over $(\mathbb N, 1, <)$, where we can quantify over sets and individual ...
71 views

### Show that a given formula is not provable without the associative rule

This question is from Shoenfield's "Mathematical Logic", an exercise on page 25. Show that the formula $((x \neq x) \vee \neg(x \neq x \vee x \neq x)) \vee (x \neq x \vee x \neq x)$ is a theorem, ...
91 views

### Can Left Conjunction Elimination Get Proven in M in Less Than 30 lines?

Peter Smith writes in his Types of Proof System: "How do you get from: $\lnot$(P -> $\lnot$ Q) to the desired conclusion P? It can be done, but as far as I know it takes well over fifty lines (if done ...
152 views

### Is there a definition of the existential quantifier which does not imply the axiom of choice?

The definition of the existential quantifer given in Bourbaki's Theory of Sets is $$(\exists x)R \iff (\tau_x(R)\mid x)R.$$ Here $x$ is a letter, $R$ is a relation, and $(\tau_x(R)\mid x)R$ means ...
66 views

112 views

### What is the root of first class object in programming languages?

What is the root of "first class object" of programming languages? (Also see https://en.wikipedia.org/wiki/First-class_function, and https://stackoverflow.com/questions/245192/what-are-first-class-...
184 views

### Connection between Algebraic structures and Formal Systems

I am a college student with very little mathematics background (up to Calculus 152 at Rutgers University), but have become increasingly interested in computing and mathematics in the last year. I am ...
64 views

### Are there any formal theories that are not axiomatic?

Are there any formal theories that are not axiomatic? Could you give me some examples?
49 views

23 views

### Can I effeciently check whether the inverse of a semantic function exists?

I'm relatively new to the fields of formal semantics/systems/languages or even model theory and therefore I miss some knowledge and experience. I try to boil the question down to the core essence of ...
35 views

### Logical systems and formal proof

Is there any good book dealing with various formal systems and a book for formal proofs. Or atleast some good notes. This page on wikipedia also says: 'This article needs attention from an expert in ...
200 views

### A question about the analogy between formal systems and Turing machines

It is well known the analogy between formal systems and Turing machines. If I am not wrong, you can code any formal system of language L in first order logic into a Turing machine, and there is a ...
77 views

### Differential fields and rings

If one is to compute the derivative of $$y=3x+2$$ by $$\frac{\mathrm{d}(3x+2)}{\mathrm{d} x}$$ Would I be working with differential fields? Since differential fields is a first-order ...
34 views

### What happens when we introduce a third 'paradox' possibility to the Halting Machine?

Thanks to Turing, we know that it is impossible to construct a machine that can prove for all machines whether they halt or not. This then has mayor implications on many other fields and theorems, ...
57 views

### Creating a formal system which corresponds to multiplication (of natural numbers)

I've begun studying mathematical logic with Hodel's 'An Introduction to Mathematical Logic', and have just learnt about formal systems and their components. In the textbook, Hodel gives as an example ...
52 views

### Is there a standard notion of a “theory of Turing machines”?

Of course, there are more-or-less standard definitions of Turing machines as a certain type of mathematical object formalized in some theory (Say, ZFC), but what I am looking for is a first order ...
35 views

### Efficiently Verifying “identities” in Arithmetic

So suppose I have two expressions $A,B$ both consisting of some combination of parenthesis $()$, addition $+$, multiplication $\times$, exponentiation $\text{^}$. What is an efficient way to check ...
64 views

### Can there be true but unprovable statements about object other than numbers?

In ZFC, everything is a pure set, and because the necessary amount of arithmetic for the Gödel's incompleteness theorems to go through is interpretable within ZFC, there are undecidable statements ...
28 views

### Simplest way to say “$\varphi$ is a wff of formal system $\mathbf{F}$”?

What is the simplest way to say "$\varphi$ is a well-formed formula of formal system $\mathbf{F}$" in symbols? The only thing that comes to mind is: $$\varphi \in \mathbf{F}$$ Am I right? I.e., ...
I want to formalize: "If X is less than Y, Then U is equal to Y ", and have been told that $$\bf [\forall V \sim X=(Y+V)]U=Y$$ does not cover the case X=Y. Therefore I have rewritten it as  \bf [\...