84:
74:
53:
389:
boolean algebras, other fragments of the classical decision problem as presented by Borger and
Gurevich, etc.). So these generalizations are something to be discussed and possibly serve as an interesting basis of an educational article that explores connections between various concepts. But saying that this is FOL with equality seems like it's going against the title and the original intention of this article?
22:
170:, as I beleive it is effectively talking about the same topic. I made the direction from there to here, since I believe that it is more commonly called "the theory of equality" in textbooks, rather than "equational logic". As the texts proceed, it is noted that the "theory of equality" or "equational theory" has some inference rules that take it beyond the
287:) universal, but not existential, quantification. The universal quantifiers are usually omitted; this may be meant in the article. On the other hand, I guess (but admittely are not sure) that there is just a single theory of pure equality and that this one doesn't use existential quantifiers. An expert in equational reasoning, like
178:
article. All this is particularly notable, since the equational theory is kind of the very first theory that is more complicated than the free theory. It's the first (simplest, smallest) theory that adds ..., well, adds inference rules! (or constraints, presentations, propositional schemas, whatever
388:
the way this is stated, this article is clear: it's FOL logic with equality but no function or predicate symbols in the signature. It's decidable (with finite model property) and, since then extended in many different directions (WSkS, congruence closure for quantifier-free fragment, FOL theory of
460:
Unlike in the theory of pure equality, equational logic permits function symbols, and function symbols are indeed their main point of interest. Since the motivation for their study and the tasks they are trying to achieve are also very different, a merger would merely confuse readers rather than
359:
Hmm. OK. Well, I guess this breaks down into 4-5 sections: a description of what Löwenheim did in 1915, how/why one wishes to have an equational logic, what prenex has to do with it, its role in SMT, and finally (for me at least) its utility in modern programming to perform "static analysis" of
187:
solvers throw in the equational theory as kind of the first non-trivial theory that they support. I'm going to let this merge proposal cool it's heels, here, to see how it is received. I'm busy doing other things, anyways.
257:
is a first-order theory so quantifiers are allowed. I agree that ideally we should have an article for the most general logic and discuss special cases as subsections. Another point of reference is
140:
441:. That article is somewhat long, so maybe some of that material can be moved here, as it is more specific than what we've added with a few (historically very spread out) edits so far.
309:
I am not sure to be an expert and you are kind to say so. I looked at my
American Heritage Dictionary and I am not fully satisfied with its definitions, but at least I see that
329:. Therefore, for me, all this discussion raises more questions that it can really address them. Therefore, for now, I am not sure that a merge is needed. --
414:
If it's decidable, does that mean any extension to 2nd-order logic that is sound with respect to
Leibniz's principle is a conservative extension of it? —
490:
130:
485:
106:
361:
189:
97:
58:
325:
is somewhat dynamic, implying a process to make sides equal. Moreover the
Knowledge articles assume that the underlying logic is
184:
404:
438:
33:
300:
236:
334:
266:
254:
224:
208:
21:
365:
330:
258:
193:
296:
232:
39:
83:
261:
which discusses the theory of uninterpreted functions like in the equational axiom example you wrote.
392:
288:
292:
262:
105:
on
Knowledge. If you would like to participate, please visit the project page, where you can join
466:
284:
89:
73:
52:
446:
400:
421:
250:
228:
204:
175:
167:
159:
179:
you want to call them, something that removes some of the freedom.) Notable also that in
430:
Not sure if it follows from that, but I made the connections to some 2nd order theories.
223:) while the latter does not. Therefore, if the articles are merged, the special article
384:
I just read this article. There may well be other related topics that are of interest,
180:
479:
462:
470:
450:
442:
425:
408:
396:
369:
338:
304:
270:
240:
197:
415:
171:
102:
79:
360:
expressions to simplify them, prior to any run-time dynamic evaluation.
15:
437:
The topic of this article is discussed in similar length in
283:
As far as I know, equational logic allows (for a formula in
211:, since the former allows for equational axioms (like ∀
174:, those inference rules are the ones described in the
101:, a collaborative effort to improve the coverage of
439:
List_of_first-order_theories#Pure_identity_theories
253:states that it does not allow quantifiers and
8:
47:
19:
49:
7:
295:) may help to clarify this issue. -
227:should become a part of the general
95:This article is within the scope of
38:It is of interest to the following
14:
491:Low-priority mathematics articles
166:I just added a merge-from tag to
115:Knowledge:WikiProject Mathematics
118:Template:WikiProject Mathematics
82:
72:
51:
20:
486:Stub-Class mathematics articles
135:This article has been rated as
185:satisfiability modulo theories
1:
339:13:45, 22 November 2021 (UTC)
305:09:36, 22 November 2021 (UTC)
271:23:34, 21 November 2021 (UTC)
241:18:19, 21 November 2021 (UTC)
198:21:19, 20 November 2021 (UTC)
109:and see a list of open tasks.
451:10:12, 5 February 2022 (UTC)
426:07:24, 5 February 2022 (UTC)
409:10:50, 4 February 2022 (UTC)
370:17:39, 1 December 2021 (UTC)
507:
471:18:34, 7 April 2022 (UTC)
134:
67:
46:
141:project's priority scale
321:is somewhat static and
255:theory of pure equality
225:Theory of pure equality
209:Theory of pure equality
98:WikiProject Mathematics
259:Uninterpreted function
203:It appears to me that
28:This article is rated
207:is more general than
162:- its the same thing.
231:, not vice versa. -
121:mathematics articles
313:is not the same as
285:prenex normal form
183:, pretty much all
90:Mathematics portal
34:content assessment
461:provide context.
424:
395:comment added by
155:
154:
151:
150:
147:
146:
498:
420:
411:
297:Jochen Burghardt
251:equational logic
233:Jochen Burghardt
229:Equational logic
205:Equational logic
176:equational logic
168:equational logic
160:Equational logic
123:
122:
119:
116:
113:
92:
87:
86:
76:
69:
68:
63:
55:
48:
31:
25:
24:
16:
506:
505:
501:
500:
499:
497:
496:
495:
476:
475:
417:Charles Stewart
390:
331:PIerre.Lescanne
289:Pierre Lescanne
164:
120:
117:
114:
111:
110:
88:
81:
61:
32:on Knowledge's
29:
12:
11:
5:
504:
502:
494:
493:
488:
478:
477:
474:
473:
454:
453:
434:
433:
432:
431:
428:
381:
380:
379:
378:
377:
376:
375:
374:
373:
372:
348:
347:
346:
345:
344:
343:
342:
341:
293:Pierre de Lyon
276:
275:
274:
273:
263:Caleb Stanford
244:
243:
181:model checking
163:
156:
153:
152:
149:
148:
145:
144:
133:
127:
126:
124:
107:the discussion
94:
93:
77:
65:
64:
56:
44:
43:
37:
26:
13:
10:
9:
6:
4:
3:
2:
503:
492:
489:
487:
484:
483:
481:
472:
468:
464:
459:
456:
455:
452:
448:
444:
440:
436:
435:
429:
427:
423:
419:
418:
413:
412:
410:
406:
402:
398:
394:
387:
383:
382:
371:
367:
363:
358:
357:
356:
355:
354:
353:
352:
351:
350:
349:
340:
336:
332:
328:
324:
320:
316:
312:
308:
307:
306:
302:
298:
294:
290:
286:
282:
281:
280:
279:
278:
277:
272:
268:
264:
260:
256:
252:
248:
247:
246:
245:
242:
238:
234:
230:
226:
222:
218:
214:
210:
206:
202:
201:
200:
199:
195:
191:
186:
182:
177:
173:
169:
161:
157:
142:
138:
132:
129:
128:
125:
108:
104:
100:
99:
91:
85:
80:
78:
75:
71:
70:
66:
60:
57:
54:
50:
45:
41:
35:
27:
23:
18:
17:
458:Oppose merge
457:
416:
391:— Preceding
385:
362:67.198.37.16
326:
322:
318:
314:
310:
220:
216:
212:
190:67.198.37.16
165:
137:Low-priority
136:
96:
62:Low‑priority
40:WikiProjects
215:.Pred(Succ(
172:free theory
112:Mathematics
103:mathematics
59:Mathematics
480:Categories
249:Actually,
158:mergefrom
30:Stub-class
327:classical
463:Felix QW
405:contribs
393:unsigned
323:equation
319:Equality
315:equation
311:equality
443:Vkuncak
397:Vkuncak
139:on the
422:(talk)
291:(User:
36:scale.
467:talk
447:talk
401:talk
366:talk
335:talk
317:.
301:talk
267:talk
237:talk
194:talk
386:but
219:))=
131:Low
482::
469:)
449:)
407:)
403:•
368:)
337:)
303:)
269:)
239:)
196:)
465:(
445:(
399:(
364:(
333:(
299:(
265:(
235:(
221:x
217:x
213:x
192:(
143:.
42::
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
