Skip to main content
user695931's user avatar
user695931's user avatar
user695931's user avatar
user695931
  • Member for 9 years
  • Last seen more than a month ago
4 votes
0 answers
86 views

Automated proof verification of metalogical theorems of first order logic

4 votes
1 answer
320 views

Haskell proof checker for FOL with equality

3 votes
2 answers
521 views

Are there axioms for metalogic?

3 votes
1 answer
418 views

Induction in proof of Rule of Substitution

2 votes
2 answers
143 views

Proof that propositional logic remains consistent after the addition of a single axiom

2 votes
1 answer
104 views

A truly rigorous textbook

2 votes
0 answers
71 views

Formal definition of a Hilbert proof system

2 votes
1 answer
139 views

Formal definition of substitution being defined in type free lambda calculus

1 vote
0 answers
265 views

Theorem on alpha conversion in type free lambda calculus

1 vote
2 answers
212 views

Substituting conjunction and disjunction symbols in equivalent propositional formulas

1 vote
1 answer
91 views

Lemma to compactness theorem for propositional logic

1 vote
1 answer
129 views

Unexpected definition of structure in predicate logic

1 vote
1 answer
140 views

Ambiguity of definition of substitution in lambda calculus

1 vote
0 answers
50 views

Lemma relating to alpha equivalence of lambda terms

1 vote
1 answer
253 views

Probability of selection without replacement and dependent removal

1 vote
1 answer
191 views

example proof using predicate calculus with equality

1 vote
1 answer
476 views

Help proving formulas in first order logic using axioms of equality

0 votes
1 answer
101 views

Replacement of operation and constant symbols in a first order theory

0 votes
2 answers
80 views

The meaning of a standalone predicate statement as an assumption or step in a formal proof

0 votes
0 answers
271 views

Inequality for integral of Dirichlet kernel

0 votes
1 answer
124 views

Thinning lemma in simply typed lambda calculus

0 votes
1 answer
136 views

The Riemann integral of a function is unaffected by changes to the value of the function at finitely many points

0 votes
0 answers
61 views

Proof that substitution of predicates in FOL formulas preserves validity

0 votes
1 answer
24 views

The nth coordinate position along a path tracing the diagonals of an infinite matrix