# Tagged Questions

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)

33 views

### Defining functions in second-order arithmetic

In ZF, a function is a special kind of set, namely a set of ordered pairs where no two pairs have the same first component but different second components. How are functions defined in SOA? Are ...
40 views

### Loops in Robinson arithmetic

In the Robinson arithmetic, I wonder how the recursive definition of addition and multiplication can be well-defined. Axiom 3 seems to prohibit other chains starting with an element which has no ...
49 views

27 views

### Given a formal system show that a variable contains more of one symbol than an initial part of that variable

Given a formal system[of 4 symbols: 0, 1, ( , ) ] with rules: You may write down 0 or 1 at any time. if strings s and t have been written down, you may write down (st). write ⊢s to mean that s can ...
62 views

### Recursive definitions in formal logic

A binary tree $T$ is either A single vertex, or A graph formed by taking two binary trees, adding a vertex, and adding an edge directed from the new vertex to the root of each binary tree. Suppose ...
74 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 ...
77 views

### How can Godel's theorem apply to every formal system?

How can Godel's theorem apply to any formal system of logic, if the truth of the theorem itself is only relative to the axioms and rule of inference that were used to generate it. In other words ...
106 views

### Analysis and formal proofs.

Ever since I started learning formal logic I've had these kind of doubts: Is analysis ever studied in a completely axiomatic/formal proofy way? What I mean is, given a set of axioms and inference ...
41 views

### Peano Arithmetic: How would this formalized statement be correct?

Using Peano Axioms I have formalized the following: x is the square of an odd prime number For some odd prime number x' , x is its square IF x is some odd prime number, THEN x is the square of x' IF ...
47 views

### Do we use Z specification language these days?

I am studying organization and properties of CAM (Content Addressable Memory) of a network switch. While searching for applications of Z, I found that there are several formalization projects ...
54 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 ...
107 views

### Can there exist a definition of 'multiplication' in Presberger Arithmetic?

According to Wikipedia, Presberger Arithmetic is the first-order theory of the natural numbers with addition. It can be proved to be consistent, complete, and decidable. Though it contains no axioms ...
64 views

### What's wrong with this proof that ZFC is consistent

If we take ZFC minus all it's axioms, we can easily prove that ZFC's first axiom is independent (because all statements are independent in a formal system without any axioms). We can then prove that ...
32 views

### Will assuming an undecidable statement result in a consistent system?

If you assume that an undecidable statement in a consistent axiomatic system is true (or false), will that new system also be consistent? For example, does $\mathsf{ZF}$ being consistent imply that ...
91 views

### Rational numbers and leibniz law

Leibniz law says $a = b \implies f(a) = f(b)$. Unfortunately this law seems to fail for rational numbers e.g. ${1 \over 2} = {2 \over 4}$ but $numerator({1 \over 2}) \neq numerator({2 \over 4})$. I ...
62 views

### Order of Parentheses is Irrelevant: Metatheorem?

Here was shown by induction that the order of parentheses is irrelevant when associativity is verified. Question: Would this be a metatheorem about the formal language (say, of ZF) where the ...
40 views

### Is there a formal system which is generally accepted, and how is it called?

I read the question at Gödel's Incompleteness Theorem -- meta-reasoning "loophole"? about Gödel's incompleteness theorem. My question is little about the contents of that other ...
85 views

### Proving the rules of a complicated game are well defined

What strategy could one use to formally model a game and prove that the rules do not lead to any self contradiction? A major example that comes to mind is Magic the Gathering. The card ...
27 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 ...