259:
There are many examples of coherent/geometric theories: all algebraic theories, such as group theory and ring theory, all essentially algebraic theories, such as category theory, the theory of fields, the theory of local rings, lattice theory, projective geometry, the theory of separably closed local
280:
Effective theorem-proving for coherent theories can, with (in relation to resolution) relative ease and clarity, be automated. As noted by Bezem et al ...the absence of
Skolemisation (introduction of new function symbols) is no real hardship, and the non-conversion to clausal form allows the
200:
202:
where I and J are disjoint collections of formulae indices that each may be infinite and the formulae φ are either atoms or negations of atoms. If all the axioms are finite (i.e., for each axiom, both I and J are finite), the theory is coherent.
55:
230:
such as G3c, special coherent implications as axioms can be converted directly to inference rules without affecting the admissibility of the structural rules (Weakening, Contraction and Cut);
316:
277:, where D is required to be an atom; in fact, they generalise the “clauses” of disjunctive logic programs, where D is allowed to be a disjunction of atoms.
240:
Coherent implications form sequents that give a
Glivenko class. In this case, the result, known as the first-order Barr’s Theorem, states that if each
195:{\displaystyle \bigwedge _{i\in I}\phi _{i,1}\vee \dots \vee \phi _{i,n_{i}}\implies \bigvee _{j\in J}\phi _{j,1}\vee \dots \vee \phi _{j,m_{j}}}
398:
363:
263:
Coherent/geometric theories are preserved by pullback along geometric morphisms between topoi (Maclane & Moerdijk 1992, chapter X);
351:
222:
list eight consequences of the above theorem that explain its significance (omitting footnotes and most references):
321:
40:
tractable. Geometric logic is capable of expressing many mathematical theories and has close connections to
52:
A theory of first-order logic is geometric if it is can be axiomatised using only axioms of the form
414:
260:
rings (aka “strictly
Henselian local rings”) and the infinitary theory of torsion abelian groups;
437:
394:
359:
274:
234:
29:
386:
369:
338:
330:
227:
373:
37:
442:
419:
431:
270:
237:
rules in a certain simple form in which only atomic formulas play a critical part”;
41:
266:
Filtered colimits in Set of models of a coherent theory T are also models of T;
390:
21:
377:(Two volumes, Oxford Logic Guides 43 & 44, 3rd volume in preparation)
334:
343:
233:
In similar terms, coherent theories are “the theories expressible by
33:
281:
structure of ordinary mathematical arguments to be better retained.
256:
0 is classically provable then it is intuitionistically provable;
211:
Every first-order theory has a coherent conservative extension.
269:
Special coherent implications ∀x. C ⊃ D generalise the
58:
244:i: 0≤i≤n is a coherent implication and the sequent
356:Sketches of an Elephant: A Topos Theory Compendium
194:
415:"Why is a geometric theory called "geometric"?"
381:Maclane, Saunders Mac; Moerdijk, Ieke (1992),
298:
219:
8:
127:
123:
342:
184:
173:
148:
132:
115:
104:
79:
63:
57:
291:
317:"Geometrisation of first-order logic"
7:
315:Dyckhoff, Roy; Negri, Sara (2015),
14:
124:
1:
383:Sheaves in Geometry and Logic
358:, Oxford University Press,
299:Dyckhoff & Negri (2015)
220:Dyckhoff & Negri (2015)
459:
322:Bulletin of Symbolic Logic
391:10.1007/978-1-4612-0927-0
16:In mathematical logic,
196:
197:
423:. November 15, 2020.
385:, Springer: Berlin,
329:(2): 123–163,
226:In the context of a
56:
301:, pp. 124–125.
38:proof-theoretically
28:, a restriction of
335:10.1017/bsl.2015.7
192:
143:
74:
24:generalisation of
400:978-1-4612-0927-0
365:978-0-19-852496-0
275:logic programming
235:natural deduction
128:
59:
30:first-order logic
450:
424:
403:
376:
352:Johnstone, Peter
347:
346:
302:
296:
228:sequent calculus
201:
199:
198:
193:
191:
190:
189:
188:
159:
158:
142:
122:
121:
120:
119:
90:
89:
73:
458:
457:
453:
452:
451:
449:
448:
447:
428:
427:
413:
410:
408:Further reading
401:
380:
366:
350:
314:
311:
306:
305:
297:
293:
288:
217:
209:
180:
169:
144:
111:
100:
75:
54:
53:
50:
18:geometric logic
12:
11:
5:
456:
454:
446:
445:
440:
430:
429:
426:
425:
420:Stack Exchange
409:
406:
405:
404:
399:
378:
364:
348:
310:
307:
304:
303:
290:
289:
287:
284:
283:
282:
278:
267:
264:
261:
257:
238:
231:
216:
213:
208:
205:
187:
183:
179:
176:
172:
168:
165:
162:
157:
154:
151:
147:
141:
138:
135:
131:
126:
118:
114:
110:
107:
103:
99:
96:
93:
88:
85:
82:
78:
72:
69:
66:
62:
49:
46:
26:coherent logic
13:
10:
9:
6:
4:
3:
2:
455:
444:
441:
439:
436:
435:
433:
422:
421:
416:
412:
411:
407:
402:
396:
392:
388:
384:
379:
375:
371:
367:
361:
357:
353:
349:
345:
340:
336:
332:
328:
324:
323:
318:
313:
312:
308:
300:
295:
292:
285:
279:
276:
272:
268:
265:
262:
258:
255:
251:
247:
243:
239:
236:
232:
229:
225:
224:
223:
221:
214:
212:
206:
204:
185:
181:
177:
174:
170:
166:
163:
160:
155:
152:
149:
145:
139:
136:
133:
129:
116:
112:
108:
105:
101:
97:
94:
91:
86:
83:
80:
76:
70:
67:
64:
60:
47:
45:
43:
39:
35:
31:
27:
23:
19:
418:
382:
355:
326:
320:
309:Bibliography
294:
271:Horn clauses
253:
249:
245:
241:
218:
215:Significance
210:
51:
42:topos theory
25:
17:
15:
248:1, . . . ,
48:Definitions
432:Categories
374:1071.18002
344:10023/6818
22:infinitary
171:ϕ
167:∨
164:⋯
161:∨
146:ϕ
137:∈
130:⋁
125:⟹
102:ϕ
98:∨
95:⋯
92:∨
77:ϕ
68:∈
61:⋀
438:Geometry
354:(2002),
36:that is
207:Theorem
32:due to
397:
372:
362:
34:Skolem
20:is an
443:Logic
286:Notes
273:from
395:ISBN
360:ISBN
252:n ⇒
387:doi
370:Zbl
339:hdl
331:doi
434::
417:.
393:,
368:,
337:,
327:21
325:,
319:,
44:.
389::
341::
333::
254:I
250:I
246:I
242:I
186:j
182:m
178:,
175:j
156:1
153:,
150:j
140:J
134:j
117:i
113:n
109:,
106:i
87:1
84:,
81:i
71:I
65:i
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.